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 3693 | . 2 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) → 𝐴 ∈ V) | |
2 | sbcex 3693 | . . 3 ⊢ ([𝐴 / 𝑥]𝜓 → 𝐴 ∈ V) | |
3 | 2 | adantl 485 | . 2 ⊢ (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓) → 𝐴 ∈ V) |
4 | dfsbcq2 3686 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ [𝐴 / 𝑥](𝜑 ∧ 𝜓))) | |
5 | dfsbcq2 3686 | . . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
6 | dfsbcq2 3686 | . . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜓)) | |
7 | 5, 6 | anbi12d 634 | . . 3 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓))) |
8 | sban 2088 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) | |
9 | 4, 7, 8 | vtoclbg 3473 | . 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓))) |
10 | 1, 3, 9 | pm5.21nii 383 | 1 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 = wceq 1543 [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-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-v 3400 df-sbc 3684 |
This theorem is referenced by: sbc3an 3752 sbcabel 3777 2nreu 4342 csbopg 4788 csbuni 4836 csbmpt12 5423 csbxp 5632 difopab 5685 sbcfung 6382 sbcfng 6520 sbcfg 6521 fmptsnd 6962 f1od2 30730 esum2dlem 31726 bnj976 32424 bnj110 32505 bnj1040 32619 csbwrecsg 35184 csboprabg 35187 csbmpo123 35188 f1omptsnlem 35193 mptsnunlem 35195 relowlpssretop 35221 csbfinxpg 35245 sbcani 35952 sbccom2lem 35968 brtrclfv2 40953 cotrclrcl 40968 frege124d 40987 sbiota1 41666 onfrALTlem5 41776 onfrALTlem4 41777 csbingVD 42118 onfrALTlem5VD 42119 onfrALTlem4VD 42120 csbxpgVD 42128 csbunigVD 42132 |
Copyright terms: Public domain | W3C validator |