Theorem eqri

Description: Infer equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 7-Oct-2017)

	Ref	Expression
Hypotheses	eqri.1	|- F/_ x A
	eqri.2	|- F/_ x B
	eqri.3	|- ( x e. A <-> x e. B )
Assertion	eqri	|- A = B

Proof

Step	Hyp	Ref	Expression
1		eqri.1	|- F/_ x A
2		eqri.2	|- F/_ x B
3		eqri.3	|- ( x e. A <-> x e. B )
4		nftru	|- F/ x T.
5	3	a1i	|- ( T. -> ( x e. A <-> x e. B ) )
6	4 1 2 5	eqrd	|- ( T. -> A = B )
7	6	mptru	|- A = B