![]() |
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 3788 | . 2 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) → 𝐴 ∈ V) | |
2 | sbcex 3788 | . . 3 ⊢ ([𝐴 / 𝑥]𝜓 → 𝐴 ∈ V) | |
3 | 2 | adantl 483 | . 2 ⊢ (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓) → 𝐴 ∈ V) |
4 | dfsbcq2 3781 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ [𝐴 / 𝑥](𝜑 ∧ 𝜓))) | |
5 | dfsbcq2 3781 | . . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
6 | dfsbcq2 3781 | . . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜓)) | |
7 | 5, 6 | anbi12d 632 | . . 3 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓))) |
8 | sban 2084 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) | |
9 | 4, 7, 8 | vtoclbg 3560 | . 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓))) |
10 | 1, 3, 9 | pm5.21nii 380 | 1 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 = wceq 1542 [wsb 2068 ∈ wcel 2107 Vcvv 3475 [wsbc 3778 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-sbc 3779 |
This theorem is referenced by: sbc3an 3848 sbcabel 3873 2nreu 4442 csbopg 4892 csbuni 4941 csbmpt12 5558 csbxp 5776 difopabOLD 5832 sbcfung 6573 sbcfng 6715 sbcfg 6716 fmptsnd 7167 csbfrecsg 8269 f1od2 31946 esum2dlem 33090 bnj976 33788 bnj110 33869 bnj1040 33983 csboprabg 36211 csbmpo123 36212 f1omptsnlem 36217 mptsnunlem 36219 relowlpssretop 36245 csbfinxpg 36269 sbcani 36976 sbccom2lem 36992 minregex 42285 brtrclfv2 42478 cotrclrcl 42493 frege124d 42512 sbiota1 43193 onfrALTlem5 43303 onfrALTlem4 43304 csbingVD 43645 onfrALTlem5VD 43646 onfrALTlem4VD 43647 csbxpgVD 43655 csbunigVD 43659 |
Copyright terms: Public domain | W3C validator |