Metamath Proof Explorer

Theorem abv

Description: The class of sets verifying a property is the universal class if and only if that property is a tautology. The reverse implication ( bj-abv ) requires fewer axioms. (Contributed by BJ, 19-Mar-2021) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 30-Aug-2024) (Proof shortened by BJ, 30-Aug-2024)

Ref Expression
Assertion abv ⊢ x | φ = V ↔ ∀ x φ

Proof

Step Hyp Ref Expression
1 dfcleq ⊢ x | φ = x | ⊤ ↔ ∀ y y ∈ x | φ ↔ y ∈ x | ⊤
2 vextru ⊢ y ∈ x | ⊤
3 2 tbt ⊢ y ∈ x | φ ↔ y ∈ x | φ ↔ y ∈ x | ⊤
4 df-clab ⊢ y ∈ x | φ ↔ y x φ
5 3 4 bitr3i ⊢ y ∈ x | φ ↔ y ∈ x | ⊤ ↔ y x φ
6 5 albii ⊢ ∀ y y ∈ x | φ ↔ y ∈ x | ⊤ ↔ ∀ y y x φ
7 1 6 bitri ⊢ x | φ = x | ⊤ ↔ ∀ y y x φ
8 dfv2 ⊢ V = x | ⊤
9 8 eqeq2i ⊢ x | φ = V ↔ x | φ = x | ⊤
10 nfv ⊢ Ⅎ y φ
11 10 sb8v ⊢ ∀ x φ ↔ ∀ y y x φ
12 7 9 11 3bitr4i ⊢ x | φ = V ↔ ∀ x φ