| 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 3906 | . 2 ⊢ (⊤ → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
| 4 | 3 | mptru 1547 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ⊤wtru 1541 ⦋csb 3899 |
| 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-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-sbc 3789 df-csb 3900 |
| This theorem is referenced by: csbnest1g 4432 csbvarg 4434 csbsng 4708 csbprg 4709 csbopg 4891 csbuni 4936 csbmpt12 5562 csbxp 5785 csbcnv 5894 csbcnvgALT 5895 csbdm 5908 csbres 6000 csbrn 6223 csbpredg 6327 csbfv12 6954 fvmpocurryd 8296 csbfrecsg 8309 csbwrecsg 8346 csbnegg 11505 csbwrdg 14582 matgsum 22443 precsexlemcbv 28230 precsexlem3 28233 disjxpin 32601 f1od2 32732 sumeq2si 36203 prodeq2si 36205 bj-csbsn 36905 csbrecsg 37329 csbrdgg 37330 csboprabg 37331 csbmpo123 37332 csbfinxpg 37389 poimirlem24 37651 cdleme31so 40381 cdleme31sn 40382 cdleme31sn1 40383 cdleme31se 40384 cdleme31se2 40385 cdleme31sc 40386 cdleme31sde 40387 cdleme31sn2 40391 cdlemkid3N 40935 cdlemkid4 40936 climinf2mpt 45729 climinfmpt 45730 |
| Copyright terms: Public domain | W3C validator |