This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality The universal class eqv
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 ↔ ∀ 𝑥 𝑥 ∈ 𝐴 )