Theorem eqv

Description: The universe contains every set. (Contributed by NM, 11-Sep-2006) Remove dependency on ax-10 , ax-11 , ax-13 . (Revised by BJ, 10-Aug-2022)

	Ref	Expression
Assertion	eqv	$$⊢A=\mathrm{V}\leftrightarrow \forall xx\in A$$

Proof

Step	Hyp	Ref	Expression
1		dfcleq	$$⊢A=\mathrm{V}\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in \mathrm{V}\right)$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	tbt	$$⊢x\in A\leftrightarrow \left(x\in A\leftrightarrow x\in \mathrm{V}\right)$$
4	3	albii	$$⊢\forall xx\in A\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in \mathrm{V}\right)$$
5	1 4	bitr4i	$$⊢A=\mathrm{V}\leftrightarrow \forall xx\in A$$