Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbcex2 | Structured version Visualization version GIF version |
Description: Move existential quantifier in and out of class substitution. (Contributed by NM, 21-May-2004.) (Revised by NM, 18-Aug-2018.) |
Ref | Expression |
---|---|
sbcex2 | ⊢ ([𝐴 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcex 3693 | . 2 ⊢ ([𝐴 / 𝑦]∃𝑥𝜑 → 𝐴 ∈ V) | |
2 | sbcex 3693 | . . 3 ⊢ ([𝐴 / 𝑦]𝜑 → 𝐴 ∈ V) | |
3 | 2 | exlimiv 1938 | . 2 ⊢ (∃𝑥[𝐴 / 𝑦]𝜑 → 𝐴 ∈ V) |
4 | dfsbcq2 3686 | . . 3 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑦]∃𝑥𝜑 ↔ [𝐴 / 𝑦]∃𝑥𝜑)) | |
5 | dfsbcq2 3686 | . . . 4 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑦]𝜑 ↔ [𝐴 / 𝑦]𝜑)) | |
6 | 5 | exbidv 1929 | . . 3 ⊢ (𝑧 = 𝐴 → (∃𝑥[𝑧 / 𝑦]𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑)) |
7 | sbex 2284 | . . 3 ⊢ ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑) | |
8 | 4, 6, 7 | vtoclbg 3473 | . 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑)) |
9 | 1, 3, 8 | pm5.21nii 383 | 1 ⊢ ([𝐴 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝐴 / 𝑦]𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1543 ∃wex 1787 [wsb 2072 ∈ wcel 2112 Vcvv 3398 [wsbc 3683 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-nf 1792 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-v 3400 df-sbc 3684 |
This theorem is referenced by: sbcabel 3777 csbuni 4836 csbxp 5632 csbdm 5751 sbcfung 6382 bnj89 32366 bnj985v 32600 bnj985 32601 csbwrecsg 35184 csboprabg 35187 sbcexf 35959 onfrALTlem5 41776 onfrALTlem5VD 42119 csbxpgVD 42128 csbrngVD 42130 csbunigVD 42132 |
Copyright terms: Public domain | W3C validator |