MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ab0orv Structured version   Visualization version   GIF version

Theorem ab0orv 4380
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.)
Assertion
Ref Expression
ab0orv ({𝑥𝜑} = V ∨ {𝑥𝜑} = ∅)
Distinct variable group:   𝜑,𝑥

Proof of Theorem ab0orv
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 nfv 1909 . . 3 𝑦𝜑
2 nf3 1780 . . 3 (Ⅎ𝑦𝜑 ↔ (∀𝑦𝜑 ∨ ∀𝑦 ¬ 𝜑))
31, 2mpbi 229 . 2 (∀𝑦𝜑 ∨ ∀𝑦 ¬ 𝜑)
4 tbtru 1541 . . . . . 6 (𝜑 ↔ (𝜑 ↔ ⊤))
5 df-clab 2703 . . . . . . . 8 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
6 sbv 2083 . . . . . . . 8 ([𝑦 / 𝑥]𝜑𝜑)
75, 6bitr2i 275 . . . . . . 7 (𝜑𝑦 ∈ {𝑥𝜑})
8 tru 1537 . . . . . . . 8
9 vextru 2709 . . . . . . . 8 𝑦 ∈ {𝑥 ∣ ⊤}
108, 92th 263 . . . . . . 7 (⊤ ↔ 𝑦 ∈ {𝑥 ∣ ⊤})
117, 10bibi12i 338 . . . . . 6 ((𝜑 ↔ ⊤) ↔ (𝑦 ∈ {𝑥𝜑} ↔ 𝑦 ∈ {𝑥 ∣ ⊤}))
124, 11bitri 274 . . . . 5 (𝜑 ↔ (𝑦 ∈ {𝑥𝜑} ↔ 𝑦 ∈ {𝑥 ∣ ⊤}))
1312albii 1813 . . . 4 (∀𝑦𝜑 ↔ ∀𝑦(𝑦 ∈ {𝑥𝜑} ↔ 𝑦 ∈ {𝑥 ∣ ⊤}))
14 dfcleq 2718 . . . 4 ({𝑥𝜑} = {𝑥 ∣ ⊤} ↔ ∀𝑦(𝑦 ∈ {𝑥𝜑} ↔ 𝑦 ∈ {𝑥 ∣ ⊤}))
15 dfv2 3464 . . . . . 6 V = {𝑥 ∣ ⊤}
1615eqcomi 2734 . . . . 5 {𝑥 ∣ ⊤} = V
1716eqeq2i 2738 . . . 4 ({𝑥𝜑} = {𝑥 ∣ ⊤} ↔ {𝑥𝜑} = V)
1813, 14, 173bitr2i 298 . . 3 (∀𝑦𝜑 ↔ {𝑥𝜑} = V)
19 equid 2007 . . . . . . 7 𝑦 = 𝑦
2019nbn3 372 . . . . . 6 𝜑 ↔ (𝜑 ↔ ¬ 𝑦 = 𝑦))
21 df-clab 2703 . . . . . . . 8 (𝑦 ∈ {𝑥 ∣ ¬ 𝑥 = 𝑥} ↔ [𝑦 / 𝑥] ¬ 𝑥 = 𝑥)
22 equid 2007 . . . . . . . . . . . 12 𝑥 = 𝑥
2322, 192th 263 . . . . . . . . . . 11 (𝑥 = 𝑥𝑦 = 𝑦)
2423notbii 319 . . . . . . . . . 10 𝑥 = 𝑥 ↔ ¬ 𝑦 = 𝑦)
2524a1i 11 . . . . . . . . 9 (𝑥 = 𝑦 → (¬ 𝑥 = 𝑥 ↔ ¬ 𝑦 = 𝑦))
2625sbievw 2087 . . . . . . . 8 ([𝑦 / 𝑥] ¬ 𝑥 = 𝑥 ↔ ¬ 𝑦 = 𝑦)
2721, 26bitr2i 275 . . . . . . 7 𝑦 = 𝑦𝑦 ∈ {𝑥 ∣ ¬ 𝑥 = 𝑥})
287, 27bibi12i 338 . . . . . 6 ((𝜑 ↔ ¬ 𝑦 = 𝑦) ↔ (𝑦 ∈ {𝑥𝜑} ↔ 𝑦 ∈ {𝑥 ∣ ¬ 𝑥 = 𝑥}))
2920, 28bitri 274 . . . . 5 𝜑 ↔ (𝑦 ∈ {𝑥𝜑} ↔ 𝑦 ∈ {𝑥 ∣ ¬ 𝑥 = 𝑥}))
3029albii 1813 . . . 4 (∀𝑦 ¬ 𝜑 ↔ ∀𝑦(𝑦 ∈ {𝑥𝜑} ↔ 𝑦 ∈ {𝑥 ∣ ¬ 𝑥 = 𝑥}))
31 dfcleq 2718 . . . 4 ({𝑥𝜑} = {𝑥 ∣ ¬ 𝑥 = 𝑥} ↔ ∀𝑦(𝑦 ∈ {𝑥𝜑} ↔ 𝑦 ∈ {𝑥 ∣ ¬ 𝑥 = 𝑥}))
32 dfnul2 4325 . . . . . 6 ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
3332eqcomi 2734 . . . . 5 {𝑥 ∣ ¬ 𝑥 = 𝑥} = ∅
3433eqeq2i 2738 . . . 4 ({𝑥𝜑} = {𝑥 ∣ ¬ 𝑥 = 𝑥} ↔ {𝑥𝜑} = ∅)
3530, 31, 343bitr2i 298 . . 3 (∀𝑦 ¬ 𝜑 ↔ {𝑥𝜑} = ∅)
3618, 35orbi12i 912 . 2 ((∀𝑦𝜑 ∨ ∀𝑦 ¬ 𝜑) ↔ ({𝑥𝜑} = V ∨ {𝑥𝜑} = ∅))
373, 36mpbi 229 1 ({𝑥𝜑} = V ∨ {𝑥𝜑} = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wo 845  wal 1531   = wceq 1533  wtru 1534  wnf 1777  [wsb 2059  wcel 2098  {cab 2702  Vcvv 3461  c0 4322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-v 3463  df-dif 3947  df-nul 4323
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator