Theorem eqvf

Description: The universe contains every set. (Contributed by BJ, 15-Jul-2021)

	Ref	Expression
Hypothesis	eqvf.1	|- F/_ x A
Assertion	eqvf	|- ( A = _V <-> A. x x e. A )

Proof

Step	Hyp	Ref	Expression
1		eqvf.1	|- F/_ x A
2		nfcv	|- F/_ x _V
3	1 2	cleqf	|- ( A = _V <-> A. x ( x e. A <-> x e. _V ) )
4		vex	|- x e. _V
5	4	tbt	|- ( x e. A <-> ( x e. A <-> x e. _V ) )
6	5	albii	|- ( A. x x e. A <-> A. x ( x e. A <-> x e. _V ) )
7	3 6	bitr4i	|- ( A = _V <-> A. x x e. A )