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

Metamath Proof Explorer

Theorem eqvf

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

Ref Expression
Hypothesis eqvf.1 ⊢ Ⅎ _ x A
Assertion eqvf ⊢ A = V ↔ ∀ x x ∈ A

Proof

Step Hyp Ref Expression
1 eqvf.1 ⊢ Ⅎ _ x A
2 nfcv ⊢ Ⅎ _ x V
3 1 2 cleqf ⊢ A = V ↔ ∀ x x ∈ A ↔ x ∈ V
4 vex ⊢ x ∈ V
5 4 tbt ⊢ x ∈ A ↔ x ∈ A ↔ x ∈ V
6 5 albii ⊢ ∀ x x ∈ A ↔ ∀ x x ∈ A ↔ x ∈ V
7 3 6 bitr4i ⊢ A = V ↔ ∀ x x ∈ A