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

Theorem sbcex2 3841
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 3786 . 2 ([𝐴 / 𝑦]𝑥𝜑𝐴 ∈ V)
2 sbcex 3786 . . 3 ([𝐴 / 𝑦]𝜑𝐴 ∈ V)
32exlimiv 1926 . 2 (∃𝑥[𝐴 / 𝑦]𝜑𝐴 ∈ V)
4 dfsbcq2 3779 . . 3 (𝑧 = 𝐴 → ([𝑧 / 𝑦]∃𝑥𝜑[𝐴 / 𝑦]𝑥𝜑))
5 dfsbcq2 3779 . . . 4 (𝑧 = 𝐴 → ([𝑧 / 𝑦]𝜑[𝐴 / 𝑦]𝜑))
65exbidv 1917 . . 3 (𝑧 = 𝐴 → (∃𝑥[𝑧 / 𝑦]𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑))
7 sbex 2271 . . 3 ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑)
84, 6, 7vtoclbg 3542 . 2 (𝐴 ∈ V → ([𝐴 / 𝑦]𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑))
91, 3, 8pm5.21nii 378 1 ([𝐴 / 𝑦]𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1534  wex 1774  [wsb 2060  wcel 2099  Vcvv 3471  [wsbc 3776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-sbc 3777
This theorem is referenced by:  sbcabel  3871  csbuni  4939  csbxp  5777  csbdm  5900  sbcfung  6577  csbfrecsg  8290  bnj89  34352  bnj985v  34584  bnj985  34585  csboprabg  36809  sbcexf  37588  onfrALTlem5  43981  onfrALTlem5VD  44324  csbxpgVD  44333  csbrngVD  44335  csbunigVD  44337
  Copyright terms: Public domain W3C validator