![]() |
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 3835 | . 2 ⊢ (⊤ → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
4 | 3 | mptru 1545 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1538 ⊤wtru 1539 ⦋csb 3828 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-sbc 3721 df-csb 3829 |
This theorem is referenced by: csbnest1g 4337 csbvarg 4339 csbsng 4604 csbprg 4605 csbopg 4783 csbuni 4829 csbmpt12 5409 csbxp 5614 csbcnv 5718 csbcnvgALT 5719 csbdm 5730 csbres 5821 csbrn 6027 csbfv12 6688 fvmpocurryd 7920 csbnegg 10872 csbwrdg 13887 matgsum 21042 disjxpin 30351 f1od2 30483 bj-csbsn 34345 csbpredg 34743 csbwrecsg 34744 csbrecsg 34745 csbrdgg 34746 csboprabg 34747 csbmpo123 34748 csbfinxpg 34805 poimirlem24 35081 cdleme31so 37675 cdleme31sn 37676 cdleme31sn1 37677 cdleme31se 37678 cdleme31se2 37679 cdleme31sc 37680 cdleme31sde 37681 cdleme31sn2 37685 cdlemkid3N 38229 cdlemkid4 38230 climinf2mpt 42356 climinfmpt 42357 |
Copyright terms: Public domain | W3C validator |