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

Metamath Proof Explorer

Theorem ab0orv

Description: The class abstraction defined by a formula not containing the abstraction variable is either the empty set or the universal class. (Contributed by Mario Carneiro, 29-Aug-2013) (Revised by BJ, 22-Mar-2020) Reduce axiom usage. (Revised by GG, 30-Aug-2024)

Ref Expression
Assertion ab0orv ⊢ x | φ = V ∨ x | φ = ∅

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ y φ
2 nf3 ⊢ Ⅎ y φ ↔ ∀ y φ ∨ ∀ y ¬ φ
3 1 2 mpbi ⊢ ∀ y φ ∨ ∀ y ¬ φ
4 biidd ⊢ x = y → φ ↔ φ
5 4 eqabcbw ⊢ x | φ = x | ⊤ ↔ ∀ y φ ↔ y ∈ x | ⊤
6 dfv2 ⊢ V = x | ⊤
7 6 eqeq2i ⊢ x | φ = V ↔ x | φ = x | ⊤
8 vextru ⊢ y ∈ x | ⊤
9 8 tbt ⊢ φ ↔ φ ↔ y ∈ x | ⊤
10 9 albii ⊢ ∀ y φ ↔ ∀ y φ ↔ y ∈ x | ⊤
11 5 7 10 3bitr4i ⊢ x | φ = V ↔ ∀ y φ
12 4 ab0w ⊢ x | φ = ∅ ↔ ∀ y ¬ φ
13 11 12 orbi12i ⊢ x | φ = V ∨ x | φ = ∅ ↔ ∀ y φ ∨ ∀ y ¬ φ
14 3 13 mpbir ⊢ x | φ = V ∨ x | φ = ∅