| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sbcim1 | Structured version Visualization version GIF version | ||
| Description: Distribution of class substitution over implication. One direction of sbcimg 3786 that holds for proper classes. (Contributed by NM, 17-Aug-2018.) Avoid ax-10 2146, ax-12 2182. (Revised by SN, 26-Oct-2024.) |
| Ref | Expression |
|---|---|
| sbcim1 | ⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbcex 3747 | . 2 ⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) → 𝐴 ∈ V) | |
| 2 | dfsbcq2 3740 | . . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ [𝐴 / 𝑥](𝜑 → 𝜓))) | |
| 3 | dfsbcq2 3740 | . . . . 5 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
| 4 | dfsbcq2 3740 | . . . . 5 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜓)) | |
| 5 | 3, 4 | imbi12d 344 | . . . 4 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓))) |
| 6 | 2, 5 | imbi12d 344 | . . 3 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) ↔ ([𝐴 / 𝑥](𝜑 → 𝜓) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)))) |
| 7 | sbi1 2076 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | |
| 8 | 6, 7 | vtoclg 3508 | . 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥](𝜑 → 𝜓) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓))) |
| 9 | 1, 8 | mpcom 38 | 1 ⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1541 [wsb 2067 ∈ wcel 2113 Vcvv 3437 [wsbc 3737 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2705 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1544 df-ex 1781 df-sb 2068 df-clab 2712 df-cleq 2725 df-clel 2808 df-v 3439 df-sbc 3738 |
| This theorem is referenced by: opsbc2ie 32459 frege59c 44042 frege60c 44043 frege62c 44045 frege65c 44048 frege70 44053 frege72 44055 frege92 44075 frege120 44103 |
| Copyright terms: Public domain | W3C validator |