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 empty set vss
Theorem vss
Description: Only the universal class has the universal class as a subclass.
(Contributed by NM , 17-Sep-2003) (Proof shortened by Andrew Salmon , 26-Jun-2011)
Ref
Expression
Assertion
vss ⊢ ( V ⊆ 𝐴 ↔ 𝐴 = V )
Proof
Step
Hyp
Ref
Expression
1
ssv ⊢ 𝐴 ⊆ V
2
1
biantrur ⊢ ( V ⊆ 𝐴 ↔ ( 𝐴 ⊆ V ∧ V ⊆ 𝐴 ) )
3
eqss ⊢ ( 𝐴 = V ↔ ( 𝐴 ⊆ V ∧ V ⊆ 𝐴 ) )
4
2 3
bitr4i ⊢ ( V ⊆ 𝐴 ↔ 𝐴 = V )