![]() |
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 | rabeq 3040 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | rabeqbidv.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | rabbidv 3038 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | eqtrd 2487 |
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 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ral 2744 df-rab 2748 |
This theorem is referenced by: elfvmptrab1 5975 elovmpt2rab1 6521 ovmpt3rab1 6530 suppval 6921 mpt2xopoveq 6970 supeq123d 7969 phival 14727 dfphi2 14734 hashbcval 14966 imasval 15423 imasvalOLD 15424 ismre 15508 mrisval 15548 isacs 15569 monfval 15649 ismon 15650 monpropd 15654 natfval 15863 isnat 15864 initoval 15904 termoval 15905 gsumvalx 16525 gsumpropd 16527 gsumress 16531 ismhm 16596 issubm 16606 issubg 16829 isnsg 16858 isgim 16938 isga 16957 cntzfval 16986 isslw 17272 isirred 17939 dfrhm2 17957 isrim0 17963 issubrg 18020 abvfval 18058 lssset 18169 islmhm 18262 islmim 18297 islbs 18311 rrgval 18523 mplval 18664 mplbaspropd 18842 ocvfval 19241 isobs 19295 dsmmval 19309 islinds 19379 dmatval 19529 scmatval 19541 cpmat 19745 cldval 20050 mretopd 20120 neifval 20127 ordtval 20217 ordtbas2 20219 ordtcnv 20229 ordtrest2 20232 cnfval 20261 cnpfval 20262 kgenval 20562 xkoval 20614 dfac14 20645 qtopval 20722 qtopval2 20723 hmeofval 20785 elmptrab 20854 fgval 20897 flimval 20990 utopval 21259 ucnval 21304 iscfilu 21315 ispsmet 21332 ismet 21350 isxmet 21351 blfvalps 21410 cncfval 21932 ishtpy 22015 isphtpy 22024 om1val 22073 cfilfval 22246 caufval 22257 cpnfval 22898 uc1pval 23102 mon1pval 23104 dchrval 24174 istrkgl 24518 israg 24754 iseqlg 24909 ttgval 24917 nbgraop 25163 isuvtx 25228 wwlk 25421 clwwlk 25506 is2wlkonot 25603 is2spthonot 25604 2wlksot 25607 2spthsot 25608 2wlkonot3v 25615 2spthonot3v 25616 vdgrfval 25635 rusgranumwlklem2 25690 numclwwlkovf 25821 numclwwlkovg 25827 numclwwlkovq 25839 numclwwlkovh 25841 numclwwlk5 25852 lnoval 26405 bloval 26434 hmoval 26463 ordtprsuni 28737 sigagenval 28974 faeval 29081 ismbfm 29086 carsgval 29147 sitgval 29177 erdszelem3 29928 erdsze 29937 kur14 29951 iscvm 29994 elgiso 30326 wlimeq12 30514 fwddifval 30941 poimirlem28 31980 istotbnd 32113 isbnd 32124 rngohomval 32215 rngoisoval 32228 idlval 32258 pridlval 32278 maxidlval 32284 igenval 32306 lshpset 32556 lflset 32637 pats 32863 llnset 33082 lplnset 33106 lvolset 33149 lineset 33315 pmapfval 33333 paddfval 33374 lhpset 33572 ldilfset 33685 ltrnfset 33694 ltrnset 33695 dilfsetN 33730 trnfsetN 33733 trnsetN 33734 diaffval 34610 diafval 34611 dicffval 34754 dochffval 34929 lpolsetN 35062 lcdfval 35168 lcdval 35169 mapdffval 35206 mapdfval 35207 isnacs 35558 mzpclval 35579 issdrg 36075 fourierdlem2 37981 fourierdlem3 37982 etransclem12 38121 etransclem33 38142 caragenval 38324 iccpval 38739 nbgrval 39416 uvtxaval 39469 vtxdgfval 39538 umgr2v2evd2 39574 ismgmhm 39887 issubmgm 39893 assintopval 39945 rnghmval 39995 isrngisom 40000 dmatALTval 40297 lcoop 40308 |
Copyright terms: Public domain | W3C validator |