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

Theorem sbc2or 3685
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 3701 (false) and sbc6 3703 (true) conclusions. This is interesting since dfsbcq 3678 and dfsbcq2 3679 (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 3679 . . . 4 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
2 eqeq2 2784 . . . . . 6 (𝑦 = 𝐴 → (𝑥 = 𝑦𝑥 = 𝐴))
32anbi1d 621 . . . . 5 (𝑦 = 𝐴 → ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝐴𝜑)))
43exbidv 1881 . . . 4 (𝑦 = 𝐴 → (∃𝑥(𝑥 = 𝑦𝜑) ↔ ∃𝑥(𝑥 = 𝐴𝜑)))
5 sb5 2206 . . . 4 ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑))
61, 4, 5vtoclbg 3482 . . 3 (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)))
76orcd 860 . 2 (𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑))))
8 pm5.15 996 . . 3 (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴𝜑)))
9 vex 3413 . . . . . . . . . 10 𝑥 ∈ V
10 eleq1 2848 . . . . . . . . . 10 (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
119, 10mpbii 225 . . . . . . . . 9 (𝑥 = 𝐴𝐴 ∈ V)
1211adantr 473 . . . . . . . 8 ((𝑥 = 𝐴𝜑) → 𝐴 ∈ V)
1312con3i 152 . . . . . . 7 𝐴 ∈ V → ¬ (𝑥 = 𝐴𝜑))
1413nexdv 1896 . . . . . 6 𝐴 ∈ V → ¬ ∃𝑥(𝑥 = 𝐴𝜑))
1511con3i 152 . . . . . . . 8 𝐴 ∈ V → ¬ 𝑥 = 𝐴)
1615pm2.21d 119 . . . . . . 7 𝐴 ∈ V → (𝑥 = 𝐴𝜑))
1716alrimiv 1887 . . . . . 6 𝐴 ∈ V → ∀𝑥(𝑥 = 𝐴𝜑))
1814, 172thd 257 . . . . 5 𝐴 ∈ V → (¬ ∃𝑥(𝑥 = 𝐴𝜑) ↔ ∀𝑥(𝑥 = 𝐴𝜑)))
1918bibi2d 335 . . . 4 𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴𝜑)) ↔ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑))))
2019orbi2d 900 . . 3 𝐴 ∈ V → ((([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴𝜑))) ↔ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑)))))
218, 20mpbii 225 . 2 𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑))))
227, 21pm2.61i 177 1 (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  wo 834  wal 1506   = wceq 1508  wex 1743  [wsb 2016  wcel 2051  Vcvv 3410  [wsbc 3676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-12 2107  ax-ext 2745
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-v 3412  df-sbc 3677
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator