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

Theorem sbcex2 3784
 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 3733 . 2 ([𝐴 / 𝑦]𝑥𝜑𝐴 ∈ V)
2 sbcex 3733 . . 3 ([𝐴 / 𝑦]𝜑𝐴 ∈ V)
32exlimiv 1931 . 2 (∃𝑥[𝐴 / 𝑦]𝜑𝐴 ∈ V)
4 dfsbcq2 3726 . . 3 (𝑧 = 𝐴 → ([𝑧 / 𝑦]∃𝑥𝜑[𝐴 / 𝑦]𝑥𝜑))
5 dfsbcq2 3726 . . . 4 (𝑧 = 𝐴 → ([𝑧 / 𝑦]𝜑[𝐴 / 𝑦]𝜑))
65exbidv 1922 . . 3 (𝑧 = 𝐴 → (∃𝑥[𝑧 / 𝑦]𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑))
7 sbex 2286 . . 3 ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑)
84, 6, 7vtoclbg 3520 . 2 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑))
91, 3, 8pm5.21nii 383 1 ([𝐴 / 𝑦]𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   = wceq 1538  ∃wex 1781  [wsb 2069   ∈ wcel 2112  Vcvv 3444  [wsbc 3723 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-sbc 3724 This theorem is referenced by:  sbcabel  3810  csbuni  4832  csbxp  5618  csbdm  5734  sbcfung  6352  bnj89  32099  bnj985v  32333  bnj985  32334  csbwrecsg  34739  csboprabg  34742  sbcexf  35546  onfrALTlem5  41235  onfrALTlem5VD  41578  csbxpgVD  41587  csbrngVD  41589  csbunigVD  41591
 Copyright terms: Public domain W3C validator