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	⊢ ( 𝐴 = V ↔ ∀ 𝑥 𝑥 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dfcleq	⊢ ( 𝐴 = V ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ V ) )
2		vex	⊢ 𝑥 ∈ V
3	2	tbt	⊢ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ V ) )
4	3	albii	⊢ ( ∀ 𝑥 𝑥 ∈ 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ V ) )
5	1 4	bitr4i	⊢ ( 𝐴 = V ↔ ∀ 𝑥 𝑥 ∈ 𝐴 )