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 ( { 𝑥 ∣ 𝜑 } = V ∨ { 𝑥 ∣ 𝜑 } = ∅ )

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑦 𝜑
2 nf3 ⊢ ( Ⅎ 𝑦 𝜑 ↔ ( ∀ 𝑦 𝜑 ∨ ∀ 𝑦 ¬ 𝜑 ) )
3 1 2 mpbi ⊢ ( ∀ 𝑦 𝜑 ∨ ∀ 𝑦 ¬ 𝜑 )
4 biidd ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜑 ) )
5 4 eqabcbw ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊤ } ↔ ∀ 𝑦 ( 𝜑 ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } ) )
6 dfv2 ⊢ V = { 𝑥 ∣ ⊤ }
7 6 eqeq2i ⊢ ( { 𝑥 ∣ 𝜑 } = V ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ⊤ } )
8 vextru ⊢ 𝑦 ∈ { 𝑥 ∣ ⊤ }
9 8 tbt ⊢ ( 𝜑 ↔ ( 𝜑 ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } ) )
10 9 albii ⊢ ( ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ( 𝜑 ↔ 𝑦 ∈ { 𝑥 ∣ ⊤ } ) )
11 5 7 10 3bitr4i ⊢ ( { 𝑥 ∣ 𝜑 } = V ↔ ∀ 𝑦 𝜑 )
12 4 ab0w ⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ ∀ 𝑦 ¬ 𝜑 )
13 11 12 orbi12i ⊢ ( ( { 𝑥 ∣ 𝜑 } = V ∨ { 𝑥 ∣ 𝜑 } = ∅ ) ↔ ( ∀ 𝑦 𝜑 ∨ ∀ 𝑦 ¬ 𝜑 ) )
14 3 13 mpbir ⊢ ( { 𝑥 ∣ 𝜑 } = V ∨ { 𝑥 ∣ 𝜑 } = ∅ )