![]() |
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 3786 | . 2 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) → 𝐴 ∈ V) | |
2 | sbcex 3786 | . . 3 ⊢ ([𝐴 / 𝑥]𝜓 → 𝐴 ∈ V) | |
3 | 2 | adantl 481 | . 2 ⊢ (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓) → 𝐴 ∈ V) |
4 | dfsbcq2 3779 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ [𝐴 / 𝑥](𝜑 ∧ 𝜓))) | |
5 | dfsbcq2 3779 | . . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
6 | dfsbcq2 3779 | . . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜓)) | |
7 | 5, 6 | anbi12d 631 | . . 3 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓))) |
8 | sban 2076 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) | |
9 | 4, 7, 8 | vtoclbg 3542 | . 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓))) |
10 | 1, 3, 9 | pm5.21nii 378 | 1 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 395 = wceq 1534 [wsb 2060 ∈ wcel 2099 Vcvv 3471 [wsbc 3776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3473 df-sbc 3777 |
This theorem is referenced by: sbc3an 3846 sbcabel 3871 2nreu 4442 csbopg 4892 csbuni 4939 csbmpt12 5559 csbxp 5777 difopabOLD 5833 sbcfung 6577 sbcfng 6719 sbcfg 6720 fmptsnd 7178 csbfrecsg 8290 f1od2 32516 esum2dlem 33711 bnj976 34408 bnj110 34489 bnj1040 34603 csboprabg 36809 csbmpo123 36810 f1omptsnlem 36815 mptsnunlem 36817 relowlpssretop 36843 csbfinxpg 36867 sbcani 37581 sbccom2lem 37597 minregex 42964 brtrclfv2 43157 cotrclrcl 43172 frege124d 43191 sbiota1 43871 onfrALTlem5 43981 onfrALTlem4 43982 csbingVD 44323 onfrALTlem5VD 44324 onfrALTlem4VD 44325 csbxpgVD 44333 csbunigVD 44337 |
Copyright terms: Public domain | W3C validator |