Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rabeqbidv | Structured version Visualization version Unicode version |
Description: Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.) |
Ref | Expression |
---|---|
rabeqbidv.1 | |
rabeqbidv.2 |
Ref | Expression |
---|---|
rabeqbidv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabeqbidv.1 | . . 3 | |
2 | 1 | rabeqdv 3194 | . 2 |
3 | rabeqbidv.2 | . . 3 | |
4 | 3 | rabbidv 3189 | . 2 |
5 | 2, 4 | eqtrd 2656 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wceq 1483 crab 2916 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rab 2921 |
This theorem is referenced by: elfvmptrab1 6305 elovmpt2rab1 6881 ovmpt3rab1 6891 suppval 7297 mpt2xopoveq 7345 supeq123d 8356 phival 15472 dfphi2 15479 hashbcval 15706 imasval 16171 ismre 16250 mrisval 16290 isacs 16312 monfval 16392 ismon 16393 monpropd 16397 natfval 16606 isnat 16607 initoval 16647 termoval 16648 gsumvalx 17270 gsumpropd 17272 gsumress 17276 ismhm 17337 issubm 17347 issubg 17594 isnsg 17623 isgim 17704 isga 17724 cntzfval 17753 isslw 18023 isirred 18699 dfrhm2 18717 isrim0 18723 issubrg 18780 abvfval 18818 lssset 18934 islmhm 19027 islmim 19062 islbs 19076 rrgval 19287 mplval 19428 mplbaspropd 19607 ocvfval 20010 isobs 20064 dsmmval 20078 islinds 20148 dmatval 20298 scmatval 20310 cpmat 20514 cldval 20827 mretopd 20896 neifval 20903 ordtval 20993 ordtbas2 20995 ordtcnv 21005 ordtrest2 21008 cnfval 21037 cnpfval 21038 kgenval 21338 xkoval 21390 dfac14 21421 qtopval 21498 qtopval2 21499 hmeofval 21561 elmptrab 21630 fgval 21674 flimval 21767 utopval 22036 ucnval 22081 iscfilu 22092 ispsmet 22109 ismet 22128 isxmet 22129 blfvalps 22188 cncfval 22691 ishtpy 22771 isphtpy 22780 om1val 22830 cfilfval 23062 caufval 23073 cpnfval 23695 uc1pval 23899 mon1pval 23901 dchrval 24959 istrkgl 25357 israg 25592 iseqlg 25747 ttgval 25755 nbgrval 26234 uvtxaval 26287 vtxdgfval 26363 vtxdeqd 26373 1egrvtxdg1 26405 umgr2v2evd2 26423 wwlks 26727 wwlksn 26729 wspthsn 26735 wwlksnon 26738 wspthsnon 26739 iswspthsnon 26741 rusgrnumwwlklem 26865 clwwlks 26879 clwwlksn 26881 numclwwlkovf 27213 numclwwlkovg 27220 numclwwlkovq 27232 numclwwlkovh 27234 lnoval 27607 bloval 27636 hmoval 27665 ordtprsuni 29965 sigagenval 30203 faeval 30309 ismbfm 30314 carsgval 30365 sitgval 30394 reprval 30688 erdszelem3 31175 erdsze 31184 kur14 31198 iscvm 31241 wlimeq12 31765 fwddifval 32269 poimirlem28 33437 istotbnd 33568 isbnd 33579 rngohomval 33763 rngoisoval 33776 idlval 33812 pridlval 33832 maxidlval 33838 igenval 33860 lshpset 34265 lflset 34346 pats 34572 llnset 34791 lplnset 34815 lvolset 34858 lineset 35024 pmapfval 35042 paddfval 35083 lhpset 35281 ldilfset 35394 ltrnfset 35403 ltrnset 35404 dilfsetN 35439 trnfsetN 35442 trnsetN 35443 diaffval 36319 diafval 36320 dicffval 36463 dochffval 36638 lpolsetN 36771 lcdfval 36877 lcdval 36878 mapdffval 36915 mapdfval 36916 isnacs 37267 mzpclval 37288 issdrg 37767 k0004val 38448 fourierdlem2 40326 fourierdlem3 40327 etransclem12 40463 etransclem33 40484 caragenval 40707 smflimlem3 40981 iccpval 41351 ismgmhm 41783 issubmgm 41789 assintopval 41841 rnghmval 41891 isrngisom 41896 dmatALTval 42189 lcoop 42200 |
Copyright terms: Public domain | W3C validator |