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 3719 | . 2 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ [𝐴 / 𝑥](𝜑 → 𝜓))) | |
2 | dfsbcq2 3719 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
3 | dfsbcq2 3719 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜓)) | |
4 | 2, 3 | imbi12d 345 | . 2 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓))) |
5 | sbim 2300 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | |
6 | 1, 4, 5 | vtoclbg 3507 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1539 [wsb 2067 ∈ wcel 2106 [wsbc 3716 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-12 2171 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-ex 1783 df-nf 1787 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-sbc 3717 |
This theorem is referenced by: sbcim1OLD 3773 sbceqalOLD 3783 sbc19.21g 3794 sbcssg 4454 iota4an 6415 sbcfung 6458 riotass2 7263 tfinds2 7710 telgsums 19594 bnj110 32838 bnj92 32842 bnj539 32871 bnj540 32872 f1omptsnlem 35507 mptsnunlem 35509 topdifinffinlem 35518 relowlpssretop 35535 rdgeqoa 35541 sbcimi 36268 cdlemkid3N 38947 cdlemkid4 38948 cdlemk35s 38951 cdlemk39s 38953 cdlemk42 38955 frege77 41548 frege116 41587 frege118 41589 sbcim2g 42158 onfrALTlem5 42162 sbcim2gVD 42495 sbcssgVD 42503 onfrALTlem5VD 42505 iccelpart 44885 |
Copyright terms: Public domain | W3C validator |