![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbconstg | Structured version Visualization version Unicode version |
Description: Substitution doesn't
affect a constant ![]() ![]() |
Ref | Expression |
---|---|
csbconstg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2603 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | csbconstgf 3387 |
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-nfc 2592 df-v 3059 df-sbc 3280 df-csb 3376 |
This theorem is referenced by: csb0 3783 sbcel1g 3788 sbceq1g 3789 sbcel2 3790 sbceq2g 3791 csbidm 3803 sbcbr 4471 sbcbr12g 4472 sbcbr1g 4473 sbcbr2g 4474 csbmpt12 4752 csbmpt2 4753 sbcrel 4943 csbcnvgALT 5041 csbres 5130 csbrn 5320 sbcfung 5628 csbfv12 5927 csbfv2g 5928 elfvmptrab 5999 csbov 6355 csbov12g 6356 csbov1g 6357 csbov2g 6358 csbwrdg 12738 gsummptif1n0 17653 coe1fzgsumdlem 18950 evl1gsumdlem 18999 rusgrasn 25729 disjpreima 28248 esum2dlem 28964 csbopg2 31771 csbwrecsg 31774 csbrecsg 31775 csbrdgg 31776 csbmpt22g 31778 f1omptsnlem 31784 relowlpssretop 31813 rdgeqoa 31819 csbfinxpg 31826 csbconstgi 32403 cdlemkid3N 34546 cdlemkid4 34547 cdlemk42 34554 brtrclfv2 36365 cotrclrcl 36380 frege77 36582 sbcel2gOLD 36951 onfrALTlem5 36953 onfrALTlem4 36954 csbfv12gALTOLD 37254 csbresgOLD 37257 onfrALTlem5VD 37323 onfrALTlem4VD 37324 csbsngVD 37331 csbxpgVD 37332 csbresgVD 37333 csbrngVD 37334 csbfv12gALTVD 37337 disjinfi 37522 iccelpart 38882 |
Copyright terms: Public domain | W3C validator |