![]() |
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 3779 | . 2 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ [𝐴 / 𝑥](𝜑 → 𝜓))) | |
2 | dfsbcq2 3779 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
3 | dfsbcq2 3779 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜓)) | |
4 | 2, 3 | imbi12d 344 | . 2 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓))) |
5 | sbim 2299 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | |
6 | 1, 4, 5 | vtoclbg 3559 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1541 [wsb 2067 ∈ wcel 2106 [wsbc 3776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-12 2171 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-sbc 3777 |
This theorem is referenced by: sbcim1OLD 3833 sbceqalOLD 3843 sbc19.21g 3854 sbcssg 4522 iota4an 6522 sbcfung 6569 riotass2 7392 tfinds2 7849 telgsums 19855 bnj110 33857 bnj92 33861 bnj539 33890 bnj540 33891 f1omptsnlem 36205 mptsnunlem 36207 topdifinffinlem 36216 relowlpssretop 36233 rdgeqoa 36239 sbcimi 36966 cdlemkid3N 39792 cdlemkid4 39793 cdlemk35s 39796 cdlemk39s 39798 cdlemk42 39800 frege77 42676 frege116 42715 frege118 42717 sbcim2g 43284 onfrALTlem5 43288 sbcim2gVD 43621 sbcssgVD 43629 onfrALTlem5VD 43631 iccelpart 46087 |
Copyright terms: Public domain | W3C validator |