| 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 3791 | . 2 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ [𝐴 / 𝑥](𝜑 → 𝜓))) | |
| 2 | dfsbcq2 3791 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
| 3 | dfsbcq2 3791 | . . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜓)) | |
| 4 | 2, 3 | imbi12d 344 | . 2 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓))) |
| 5 | sbim 2303 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | |
| 6 | 1, 4, 5 | vtoclbg 3557 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 [wsb 2064 ∈ wcel 2108 [wsbc 3788 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-sbc 3789 |
| This theorem is referenced by: sbcim1OLD 3843 sbceqalOLD 3852 sbc19.21g 3862 sbcssg 4520 iota4an 6543 sbcfung 6590 riotass2 7418 tfinds2 7885 telgsums 20011 bnj110 34872 bnj92 34876 bnj539 34905 bnj540 34906 f1omptsnlem 37337 mptsnunlem 37339 topdifinffinlem 37348 relowlpssretop 37365 rdgeqoa 37371 sbcimi 38117 cdlemkid3N 40935 cdlemkid4 40936 cdlemk35s 40939 cdlemk39s 40941 cdlemk42 40943 frege77 43953 frege116 43992 frege118 43994 sbcim2g 44558 onfrALTlem5 44562 sbcim2gVD 44895 sbcssgVD 44903 onfrALTlem5VD 44905 iccelpart 47420 |
| Copyright terms: Public domain | W3C validator |