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 3412 | . 2 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) → 𝐴 ∈ V) | |
2 | sbcex 3412 | . . 3 ⊢ ([𝐴 / 𝑥]𝜓 → 𝐴 ∈ V) | |
3 | 2 | adantl 481 | . 2 ⊢ (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓) → 𝐴 ∈ V) |
4 | dfsbcq2 3405 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ [𝐴 / 𝑥](𝜑 ∧ 𝜓))) | |
5 | dfsbcq2 3405 | . . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
6 | dfsbcq2 3405 | . . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜓)) | |
7 | 5, 6 | anbi12d 743 | . . 3 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓))) |
8 | sban 2387 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) | |
9 | 4, 7, 8 | vtoclbg 3240 | . 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓))) |
10 | 1, 3, 9 | pm5.21nii 367 | 1 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 = wceq 1475 [wsb 1867 ∈ wcel 1977 Vcvv 3173 [wsbc 3402 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-v 3175 df-sbc 3403 |
This theorem is referenced by: sbc3an 3461 sbcabel 3483 csbopg 4358 csbuni 4402 csbmpt12 4934 csbxp 5123 difopab 5175 sbcfung 5827 sbcfng 5955 sbcfg 5956 fmptsnd 6340 f1od2 28887 esum2dlem 29481 bnj976 30102 bnj110 30182 bnj1040 30294 csbwrecsg 32349 csboprabg 32352 csbmpt22g 32353 f1omptsnlem 32359 mptsnunlem 32361 relowlpssretop 32388 csbfinxpg 32401 sbcani 33080 sbccom2lem 33099 brtrclfv2 37038 cotrclrcl 37053 frege124d 37072 sbiota1 37657 onfrALTlem5 37778 onfrALTlem4 37779 |
Copyright terms: Public domain | W3C validator |