![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbeq2i | Structured version Visualization version Unicode version |
Description: Formula-building inference rule 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 3793 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | trud 1464 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-sbc 3280 df-csb 3376 |
This theorem is referenced by: csbnest1g 3802 csbvarg 3804 csbsng 4042 csbprg 4043 csbuni 4240 csbmpt12 4749 csbxp 4935 csbcnv 5037 csbcnvgALT 5038 csbdm 5048 csbres 5127 csbrn 5316 csbfv12 5923 fvmpt2curryd 7044 csbnegg 9898 csbwrdg 12732 matgsum 19511 disjxpin 28247 bj-csbsn 31551 csbopg2 31770 csbpredg 31772 csbwrecsg 31773 csbrecsg 31774 csbrdgg 31775 csboprabg 31776 csbmpt22g 31777 csbfinxpg 31825 poimirlem24 32009 cdleme31so 33991 cdleme31sn 33992 cdleme31sn1 33993 cdleme31se 33994 cdleme31se2 33995 cdleme31sc 33996 cdleme31sde 33997 cdleme31sn2 34001 cdlemkid3N 34545 cdlemkid4 34546 csbunigOLD 37252 csbfv12gALTOLD 37253 csbxpgOLD 37254 csbresgOLD 37256 csbrngOLD 37257 csbima12gALTOLD 37258 |
Copyright terms: Public domain | W3C validator |