![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rabeq | Structured version Visualization version Unicode version |
Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) |
Ref | Expression |
---|---|
rabeq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2592 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfcv 2592 |
. 2
![]() ![]() ![]() ![]() | |
3 | 1, 2 | rabeqf 3037 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-rab 2746 |
This theorem is referenced by: rabeqdv 3039 rabeqbidv 3040 rabeqbidva 3041 difeq1 3544 ifeq1 3885 ifeq2 3886 rabsnif 4041 elfvmptrab 5971 supp0 6919 suppvalfn 6921 suppsnop 6928 fnsuppres 6942 pmvalg 7483 supeq2 7962 oieq2 8028 cantnffval 8168 scott0 8357 hsmex2 8863 iooval2 11669 fzval2 11787 hashbc 12616 elovmpt2wrd 12709 phimullem 14727 mrcfval 15514 ipoval 16400 pmtrfval 17091 psgnfval 17141 pmtrsn 17160 lspfval 18196 lsppropd 18241 rrgval 18511 aspval 18552 psrval 18586 mvrfval 18644 ltbval 18695 opsrval 18698 dsmmbas2 19300 dsmmelbas 19302 frlmbas 19318 m1detdiag 19622 clsfval 20040 ordtrest 20218 ordtrest2lem 20219 ordtrest2 20220 isptfin 20531 islocfin 20532 xkoval 20602 xkopt 20670 qtopres 20713 kqval 20741 tsmsval2 21144 cncfval 21920 isphtpy 22012 cfilfval 22234 iscmet 22254 ttgval 24905 isumgra 25042 isuslgra 25070 isusgra 25071 edgss 25079 wwlkn 25410 clwwlkn 25495 clwwlknprop 25500 hashecclwwlkn1 25562 usghashecclwwlk 25563 rusgrasn 25673 numclwwlkovf2 25812 numclwwlkqhash 25828 ordtprsval 28724 ordtrestNEW 28727 ordtrest2NEWlem 28728 omsval 29117 omsvalOLD 29121 orrvcval4 29297 orrvcoel 29298 orrvccel 29299 snmlfval 30053 funray 30907 fvray 30908 itg2addnclem2 31994 cntotbnd 32128 docaffvalN 34689 docafvalN 34690 lcfr 35153 hlhilocv 35528 pellfundval 35727 pellfundvalOLD 35728 elmnc 35995 rgspnval 36034 rabeqd 37377 dvnprodlem1 37821 dvnprodlem2 37822 dvnprodlem3 37823 dvnprod 37824 uvtxa0 39466 cusgredg 39492 isfusgra 39789 usgfis 39811 usgfisALT 39815 assintopmap 39895 rmsuppss 40208 mndpsuppss 40209 scmsuppss 40210 dmatALTval 40246 dmatALTbas 40247 |
Copyright terms: Public domain | W3C validator |