Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbcimg | Structured version Visualization version GIF version |
Description: Distribution of class substitution over implication. (Contributed by NM, 16-Jan-2004.) |
Ref | Expression |
---|---|
sbcimg | ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsbcq2 3774 | . 2 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ [𝐴 / 𝑥](𝜑 → 𝜓))) | |
2 | dfsbcq2 3774 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
3 | dfsbcq2 3774 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜓)) | |
4 | 2, 3 | imbi12d 347 | . 2 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓))) |
5 | sbim 2307 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | |
6 | 1, 4, 5 | vtoclbg 3568 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1533 [wsb 2065 ∈ wcel 2110 [wsbc 3771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-sbc 3772 |
This theorem is referenced by: sbcim1 3824 sbceqal 3834 sbc19.21g 3845 sbcssg 4462 iota4an 6336 sbcfung 6378 riotass2 7143 tfinds2 7577 telgsums 19112 bnj110 32130 bnj92 32134 bnj539 32163 bnj540 32164 f1omptsnlem 34616 mptsnunlem 34618 topdifinffinlem 34627 relowlpssretop 34644 rdgeqoa 34650 sbcimi 35387 cdlemkid3N 38068 cdlemkid4 38069 cdlemk35s 38072 cdlemk39s 38074 cdlemk42 38076 frege77 40284 frege116 40323 frege118 40325 sbcim2g 40870 onfrALTlem5 40874 sbcim2gVD 41207 sbcssgVD 41215 onfrALTlem5VD 41217 iccelpart 43592 |
Copyright terms: Public domain | W3C validator |