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

Theorem sbcex2 3762
Description: Move existential quantifier in and out of class substitution. (Contributed by NM, 21-May-2004.) (Revised by NM, 18-Aug-2018.)
Assertion
Ref Expression
sbcex2 ([𝐴 / 𝑦]𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑)
Distinct variable groups:   𝑥,𝐴   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑦)

Proof of Theorem sbcex2
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 sbcex 3716 . 2 ([𝐴 / 𝑦]𝑥𝜑𝐴 ∈ V)
2 sbcex 3716 . . 3 ([𝐴 / 𝑦]𝜑𝐴 ∈ V)
32exlimiv 1908 . 2 (∃𝑥[𝐴 / 𝑦]𝜑𝐴 ∈ V)
4 dfsbcq2 3709 . . 3 (𝑧 = 𝐴 → ([𝑧 / 𝑦]∃𝑥𝜑[𝐴 / 𝑦]𝑥𝜑))
5 dfsbcq2 3709 . . . 4 (𝑧 = 𝐴 → ([𝑧 / 𝑦]𝜑[𝐴 / 𝑦]𝜑))
65exbidv 1899 . . 3 (𝑧 = 𝐴 → (∃𝑥[𝑧 / 𝑦]𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑))
7 sbex 2254 . . 3 ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑)
84, 6, 7vtoclbg 3511 . 2 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑))
91, 3, 8pm5.21nii 380 1 ([𝐴 / 𝑦]𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1522  wex 1761  [wsb 2042  wcel 2081  Vcvv 3437  [wsbc 3706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-v 3439  df-sbc 3707
This theorem is referenced by:  sbcabel  3789  csbuni  4773  csbxp  5536  csbdm  5652  sbcfung  6249  bnj89  31608  bnj985  31841  csbwrecsg  34139  csboprabg  34142  sbcexf  34925  onfrALTlem5  40415  onfrALTlem5VD  40758  csbxpgVD  40767  csbrngVD  40769  csbunigVD  40771
  Copyright terms: Public domain W3C validator