This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = V ↔ ∀ x x ∈ A

Proof

Step Hyp Ref Expression
1 dfcleq ⊢ A = V ↔ ∀ x x ∈ A ↔ x ∈ V
2 vex ⊢ x ∈ V
3 2 tbt ⊢ x ∈ A ↔ x ∈ A ↔ x ∈ V
4 3 albii ⊢ ∀ x x ∈ A ↔ ∀ x x ∈ A ↔ x ∈ V
5 1 4 bitr4i ⊢ A = V ↔ ∀ x x ∈ A