Theorem eqvf

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

	Ref	Expression
Hypothesis	eqvf.1	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	eqvf	$$⊢A=\mathrm{V}\leftrightarrow \forall xx\in A$$

Proof

Step	Hyp	Ref	Expression
1		eqvf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{V}$$
3	1 2	cleqf	$$⊢A=\mathrm{V}\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in \mathrm{V}\right)$$
4		vex	$$⊢x\in \mathrm{V}$$
5	4	tbt	$$⊢x\in A\leftrightarrow \left(x\in A\leftrightarrow x\in \mathrm{V}\right)$$
6	5	albii	$$⊢\forall xx\in A\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in \mathrm{V}\right)$$
7	3 6	bitr4i	$$⊢A=\mathrm{V}\leftrightarrow \forall xx\in A$$