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

Theorem sbc2or 3653
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 3669 (false) and sbc6 3671 (true) conclusions. This is interesting since dfsbcq 3646 and dfsbcq2 3647 (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 3647 . . . 4 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
2 eqeq2 2828 . . . . . 6 (𝑦 = 𝐴 → (𝑥 = 𝑦𝑥 = 𝐴))
32anbi1d 617 . . . . 5 (𝑦 = 𝐴 → ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝐴𝜑)))
43exbidv 2012 . . . 4 (𝑦 = 𝐴 → (∃𝑥(𝑥 = 𝑦𝜑) ↔ ∃𝑥(𝑥 = 𝐴𝜑)))
5 sb5 2287 . . . 4 ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑))
61, 4, 5vtoclbg 3471 . . 3 (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)))
76orcd 891 . 2 (𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑))))
8 pm5.15 1027 . . 3 (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴𝜑)))
9 vex 3405 . . . . . . . . . 10 𝑥 ∈ V
10 eleq1 2884 . . . . . . . . . 10 (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
119, 10mpbii 224 . . . . . . . . 9 (𝑥 = 𝐴𝐴 ∈ V)
1211adantr 468 . . . . . . . 8 ((𝑥 = 𝐴𝜑) → 𝐴 ∈ V)
1312con3i 151 . . . . . . 7 𝐴 ∈ V → ¬ (𝑥 = 𝐴𝜑))
1413nexdv 2027 . . . . . 6 𝐴 ∈ V → ¬ ∃𝑥(𝑥 = 𝐴𝜑))
1511con3i 151 . . . . . . . 8 𝐴 ∈ V → ¬ 𝑥 = 𝐴)
1615pm2.21d 119 . . . . . . 7 𝐴 ∈ V → (𝑥 = 𝐴𝜑))
1716alrimiv 2018 . . . . . 6 𝐴 ∈ V → ∀𝑥(𝑥 = 𝐴𝜑))
1814, 172thd 256 . . . . 5 𝐴 ∈ V → (¬ ∃𝑥(𝑥 = 𝐴𝜑) ↔ ∀𝑥(𝑥 = 𝐴𝜑)))
1918bibi2d 333 . . . 4 𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴𝜑)) ↔ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑))))
2019orbi2d 930 . . 3 𝐴 ∈ V → ((([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴𝜑))) ↔ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑)))))
218, 20mpbii 224 . 2 𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑))))
227, 21pm2.61i 176 1 (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  wal 1635   = wceq 1637  wex 1859  [wsb 2061  wcel 2157  Vcvv 3402  [wsbc 3644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-12 2215  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-v 3404  df-sbc 3645
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator