| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > csbeq2i | Structured version Visualization version GIF version | ||
| Description: Formula-building inference for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
| Ref | Expression |
|---|---|
| csbeq2i.1 | ⊢ 𝐵 = 𝐶 |
| Ref | Expression |
|---|---|
| csbeq2i | ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | csbeq2i.1 | . . . 4 ⊢ 𝐵 = 𝐶 | |
| 2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → 𝐵 = 𝐶) |
| 3 | 2 | csbeq2dv 3862 | . 2 ⊢ (⊤ → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
| 4 | 3 | mptru 1570 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1563 ⊤wtru 1564 ⦋csb 3855 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-tru 1566 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-sbc 3748 df-csb 3856 |
| This theorem is referenced by: csbnest1g 4389 csbvarg 4391 csbsng 4670 csbprg 4671 csbopg 4851 csbuni 4898 csbmpt12 5532 csbxp 5752 csbcnv 5862 csbcnvOLD 5863 csbcnvgALTOLD 5864 csbdm 5877 csbres 5971 csbrn 6193 csbpredg 6297 csbfv12 6916 fvmpocurryd 8255 csbfrecsg 8269 csbwrecsg 8303 csbnegg 11442 csbwrdg 14569 matgsum 22551 precsexlemcbv 28353 precsexlem3 28356 disjxpin 32839 f1od2 32972 sumeq2si 36570 prodeq2si 36572 bj-csbsn 37396 csbrecsg 37829 csbrdgg 37830 csboprabg 37831 csbmpo123 37832 csbfinxpg 37889 poimirlem24 38150 cdleme31so 41010 cdleme31sn 41011 cdleme31sn1 41012 cdleme31se 41013 cdleme31se2 41014 cdleme31sc 41015 cdleme31sde 41016 cdleme31sn2 41020 cdlemkid3N 41564 cdlemkid4 41565 climinf2mpt 46287 climinfmpt 46288 |
| Copyright terms: Public domain | W3C validator |