![]() |
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 4218 | . 2 ⊢ (⊤ → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
4 | 3 | mptru 1664 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1656 ⊤wtru 1657 ⦋csb 3757 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-sbc 3663 df-csb 3758 |
This theorem is referenced by: csbnest1g 4227 csbvarg 4229 csbsng 4464 csbprg 4465 csbopg 4643 csbuni 4690 csbmpt12 5238 csbxp 5439 csbcnv 5542 csbcnvgALT 5543 csbdm 5554 csbres 5636 csbrn 5841 csbfv12 6481 fvmpt2curryd 7667 csbnegg 10605 csbwrdg 13611 matgsum 20617 disjxpin 29944 f1od2 30043 bj-csbsn 33419 csbpredg 33717 csbwrecsg 33718 csbrecsg 33719 csbrdgg 33720 csboprabg 33721 csbmpt22g 33722 csbfinxpg 33769 poimirlem24 33976 cdleme31so 36453 cdleme31sn 36454 cdleme31sn1 36455 cdleme31se 36456 cdleme31se2 36457 cdleme31sc 36458 cdleme31sde 36459 cdleme31sn2 36463 cdlemkid3N 37007 cdlemkid4 37008 climinf2mpt 40739 climinfmpt 40740 |
Copyright terms: Public domain | W3C validator |