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 3892 | . 2 ⊢ (⊤ → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
4 | 3 | mptru 1544 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 ⊤wtru 1538 ⦋csb 3885 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-12 2177 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-sbc 3775 df-csb 3886 |
This theorem is referenced by: csbnest1g 4383 csbvarg 4385 csbsng 4646 csbprg 4647 csbopg 4823 csbuni 4869 csbmpt12 5446 csbxp 5652 csbcnv 5756 csbcnvgALT 5757 csbdm 5768 csbres 5858 csbrn 6062 csbfv12 6715 fvmpocurryd 7939 csbnegg 10885 csbwrdg 13897 matgsum 21048 disjxpin 30340 f1od2 30459 bj-csbsn 34223 csbpredg 34609 csbwrecsg 34610 csbrecsg 34611 csbrdgg 34612 csboprabg 34613 csbmpo123 34614 csbfinxpg 34671 poimirlem24 34918 cdleme31so 37517 cdleme31sn 37518 cdleme31sn1 37519 cdleme31se 37520 cdleme31se2 37521 cdleme31sc 37522 cdleme31sde 37523 cdleme31sn2 37527 cdlemkid3N 38071 cdlemkid4 38072 climinf2mpt 42002 climinfmpt 42003 |
Copyright terms: Public domain | W3C validator |