Theorem eqri ≪ | index | src | ≫

theorem eqri (A B: set) {x: nat}: $ x e. A <-> x e. B $ > $ A == B $;

Step	Hyp	Ref	Expression
1		hyp h	x e. A <-> x e. B
2	1	ax_gen	A. x (x e. A <-> x e. B)
3	2	conv eqs	A == B

Axiom use

axs_pred_calc (ax_gen)