![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > rabeqbidv | Structured 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 3070 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 16 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | rabeqbidv.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | rabbidv 3068 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | eqtrd 2495 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ral 2803 df-rab 2807 |
This theorem is referenced by: suppval 6801 mpt2xopoveq 6845 supeq123d 7810 phival 13959 dfphi2 13966 hashbcval 14180 imasval 14567 ismre 14646 mrisval 14686 isacs 14707 monfval 14789 ismon 14790 monpropd 14794 natfval 14974 isnat 14975 coafval 15050 ismhm 15584 issubm 15593 gsumvalx 15620 gsumpropd 15622 gsumress 15625 issubg 15799 isnsg 15828 isgim 15908 isga 15927 cntzfval 15956 isslw 16227 dprdval 16606 dprdvalOLD 16608 isirred 16913 dfrhm2 16930 isrim0 16935 issubrg 16987 abvfval 17025 lssset 17137 islmhm 17230 islmim 17265 islbs 17279 rrgval 17480 mplval 17624 mplbaspropd 17814 ocvfval 18215 isobs 18269 dsmmval 18283 islinds 18362 cldval 18758 mretopd 18827 neifval 18834 ordtval 18924 ordtbas2 18926 ordtcnv 18936 ordtrest2 18939 cnfval 18968 cnpfval 18969 kgenval 19239 xkoval 19291 dfac14 19322 qtopval 19399 qtopval2 19400 hmeofval 19462 elmptrab 19531 fgval 19574 flimval 19667 utopval 19938 ucnval 19983 iscfilu 19994 ispsmet 20011 ismet 20029 isxmet 20030 blfvalps 20089 cncfval 20595 ishtpy 20675 isphtpy 20684 om1val 20733 cfilfval 20906 caufval 20917 cpnfval 21538 uc1pval 21743 mon1pval 21745 dchrval 22705 istrkgl 23051 israg 23233 ttgval 23272 isausgra 23429 usgraeq12d 23435 usgra0v 23441 usgra1v 23459 nbgraop 23486 isuvtx 23547 vdgrfval 23716 lnoval 24303 bloval 24332 hmoval 24361 ordtprsuni 26493 ordtcnvNEW 26494 sigagenval 26727 faeval 26805 ismbfm 26810 sitgval 26861 erdszelem3 27224 erdsze 27233 kur14 27247 iscvm 27291 elgiso 27458 wlimeq12 27899 istotbnd 28815 isbnd 28826 rngohomval 28917 rngoisoval 28930 idlval 28960 pridlval 28980 maxidlval 28986 igenval 29008 isnacs 29187 mzpclval 29208 issdrg 29701 elfvmptrab1 30301 elovmpt2rab1 30306 ovmpt3rab1 30308 wwlk 30462 is2wlkonot 30529 is2spthonot 30530 2wlksot 30533 2spthsot 30534 2wlkonot3v 30541 2spthonot3v 30542 clwwlk 30576 rusgranumwlklem2 30715 numclwwlkovf 30821 numclwwlkovg 30827 numclwwlkovq 30839 numclwwlkovh 30841 numclwwlk5 30852 lcoop 31063 cpmat 31184 lshpset 32946 lflset 33027 pats 33253 llnset 33472 lplnset 33496 lvolset 33539 lineset 33705 pmapfval 33723 paddfval 33764 pclfvalN 33856 lhpset 33962 ldilfset 34075 ltrnfset 34084 ltrnset 34085 dilfsetN 34119 trnfsetN 34122 trnsetN 34123 diaffval 34998 diafval 34999 dicffval 35142 dochffval 35317 lpolsetN 35450 lcdfval 35556 lcdval 35557 mapdffval 35594 mapdfval 35595 |
Copyright terms: Public domain | W3C validator |