Theorem sbcex2 3834

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.

Step	Hyp	Ref	Expression
1		sbcex 3782	. 2 ⊢ ([𝐴 / 𝑦]∃𝑥𝜑 → 𝐴 ∈ V)
2		sbcex 3782	. . 3 ⊢ ([𝐴 / 𝑦]𝜑 → 𝐴 ∈ V)
3	2	exlimiv 1931	. 2 ⊢ (∃𝑥[𝐴 / 𝑦]𝜑 → 𝐴 ∈ V)
4		dfsbcq2 3775	. . 3 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑦]∃𝑥𝜑 ↔ [𝐴 / 𝑦]∃𝑥𝜑))
5		dfsbcq2 3775	. . . 4 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑦]𝜑 ↔ [𝐴 / 𝑦]𝜑))
6	5	exbidv 1922	. . 3 ⊢ (𝑧 = 𝐴 → (∃𝑥[𝑧 / 𝑦]𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑))
7		sbex 2288	. . 3 ⊢ ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑)
8	4, 6, 7	vtoclbg 3569	. 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑))
9	1, 3, 8	pm5.21nii 382	1 ⊢ ([𝐴 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑)

Syntax hints:   ↔ wb 208   = wceq 1537  ∃wex 1780  [wsb 2069   ∈ wcel 2114  Vcvv 3494  [wsbc 3772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3496  df-sbc 3773

This theorem is referenced by:  sbcabel  3861  csbuni  4867  csbxp  5650  csbdm  5766  sbcfung  6379  bnj89  31991  bnj985v  32225  bnj985  32226  csbwrecsg  34611  csboprabg  34614  sbcexf  35408  onfrALTlem5  40896  onfrALTlem5VD  41239  csbxpgVD  41248  csbrngVD  41250  csbunigVD  41252