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

Theorem sbc2or 3477
Description: The disjunction of two equivalences for class substitution does not require a class existence hypothesis. This theorem tells us that there are only 2 possibilities for [𝐴 / 𝑥]𝜑 behavior at proper classes, matching the sbc5 3493 (false) and sbc6 3495 (true) conclusions. This is interesting since dfsbcq 3470 and dfsbcq2 3471 (from which it is derived) do not appear to say anything obvious about proper class behavior. Note that this theorem does not tell us that it is always one or the other at proper classes; it could "flip" between false (the first disjunct) and true (the second disjunct) as a function of some other variable 𝑦 that 𝜑 or 𝐴 may contain. (Contributed by NM, 11-Oct-2004.) (Proof modification is discouraged.)
Assertion
Ref Expression
sbc2or (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑)))
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem sbc2or
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dfsbcq2 3471 . . . 4 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
2 eqeq2 2662 . . . . . 6 (𝑦 = 𝐴 → (𝑥 = 𝑦𝑥 = 𝐴))
32anbi1d 741 . . . . 5 (𝑦 = 𝐴 → ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝐴𝜑)))
43exbidv 1890 . . . 4 (𝑦 = 𝐴 → (∃𝑥(𝑥 = 𝑦𝜑) ↔ ∃𝑥(𝑥 = 𝐴𝜑)))
5 sb5 2458 . . . 4 ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑))
61, 4, 5vtoclbg 3298 . . 3 (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)))
76orcd 406 . 2 (𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑))))
8 pm5.15 951 . . 3 (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴𝜑)))
9 vex 3234 . . . . . . . . . 10 𝑥 ∈ V
10 eleq1 2718 . . . . . . . . . 10 (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
119, 10mpbii 223 . . . . . . . . 9 (𝑥 = 𝐴𝐴 ∈ V)
1211adantr 480 . . . . . . . 8 ((𝑥 = 𝐴𝜑) → 𝐴 ∈ V)
1312con3i 150 . . . . . . 7 𝐴 ∈ V → ¬ (𝑥 = 𝐴𝜑))
1413nexdv 1904 . . . . . 6 𝐴 ∈ V → ¬ ∃𝑥(𝑥 = 𝐴𝜑))
1511con3i 150 . . . . . . . 8 𝐴 ∈ V → ¬ 𝑥 = 𝐴)
1615pm2.21d 118 . . . . . . 7 𝐴 ∈ V → (𝑥 = 𝐴𝜑))
1716alrimiv 1895 . . . . . 6 𝐴 ∈ V → ∀𝑥(𝑥 = 𝐴𝜑))
1814, 172thd 255 . . . . 5 𝐴 ∈ V → (¬ ∃𝑥(𝑥 = 𝐴𝜑) ↔ ∀𝑥(𝑥 = 𝐴𝜑)))
1918bibi2d 331 . . . 4 𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴𝜑)) ↔ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑))))
2019orbi2d 738 . . 3 𝐴 ∈ V → ((([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴𝜑))) ↔ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑)))))
218, 20mpbii 223 . 2 𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑))))
227, 21pm2.61i 176 1 (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  wal 1521   = wceq 1523  wex 1744  [wsb 1937  wcel 2030  Vcvv 3231  [wsbc 3468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233  df-sbc 3469
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator