Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbcan | Structured version Visualization version GIF version |
Description: Distribution of class substitution over conjunction. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 17-Aug-2018.) |
Ref | Expression |
---|---|
sbcan | ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcex 3781 | . 2 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) → 𝐴 ∈ V) | |
2 | sbcex 3781 | . . 3 ⊢ ([𝐴 / 𝑥]𝜓 → 𝐴 ∈ V) | |
3 | 2 | adantl 484 | . 2 ⊢ (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓) → 𝐴 ∈ V) |
4 | dfsbcq2 3774 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ [𝐴 / 𝑥](𝜑 ∧ 𝜓))) | |
5 | dfsbcq2 3774 | . . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
6 | dfsbcq2 3774 | . . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜓)) | |
7 | 5, 6 | anbi12d 632 | . . 3 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓))) |
8 | sban 2082 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) | |
9 | 4, 7, 8 | vtoclbg 3568 | . 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓))) |
10 | 1, 3, 9 | pm5.21nii 382 | 1 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 = wceq 1533 [wsb 2065 ∈ wcel 2110 Vcvv 3494 [wsbc 3771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-v 3496 df-sbc 3772 |
This theorem is referenced by: sbc3an 3837 sbcabel 3860 2nreu 4392 csbopg 4820 csbuni 4866 csbmpt12 5443 csbxp 5649 difopab 5701 sbcfung 6378 sbcfng 6510 sbcfg 6511 fmptsnd 6930 f1od2 30456 esum2dlem 31351 bnj976 32049 bnj110 32130 bnj1040 32244 csbwrecsg 34607 csboprabg 34610 csbmpo123 34611 f1omptsnlem 34616 mptsnunlem 34618 relowlpssretop 34644 csbfinxpg 34668 sbcani 35385 sbccom2lem 35401 brtrclfv2 40070 cotrclrcl 40085 frege124d 40104 sbiota1 40764 onfrALTlem5 40874 onfrALTlem4 40875 csbingVD 41216 onfrALTlem5VD 41217 onfrALTlem4VD 41218 csbxpgVD 41226 csbunigVD 41230 |
Copyright terms: Public domain | W3C validator |