Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rabeqbidv | Structured version Visualization version GIF 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 3482 | . 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) |
3 | rabeqbidv.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 3 | rabbidv 3478 | . 2 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) |
5 | 2, 4 | eqtrd 2853 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 {crab 3139 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-rab 3144 |
This theorem is referenced by: elfvmptrab1w 6786 elfvmptrab1 6787 fvmptrabfv 6791 elovmporab1w 7381 elovmporab1 7382 ovmpt3rab1 7392 suppval 7821 mpoxopoveq 7874 supeq123d 8902 phival 16092 dfphi2 16099 hashbcval 16326 imasval 16772 ismre 16849 mrisval 16889 isacs 16910 monfval 16990 ismon 16991 monpropd 16995 natfval 17204 isnat 17205 initoval 17245 termoval 17246 gsumvalx 17874 gsumpropd 17876 gsumress 17880 ismhm 17946 issubm 17956 issubg 18217 isnsg 18245 isgim 18340 isga 18359 cntzfval 18388 isslw 18662 isirred 19378 dfrhm2 19398 isrim0 19404 issubrg 19464 issdrg 19503 abvfval 19518 lssset 19634 islmhm 19728 islmim 19763 islbs 19777 rrgval 19988 mplval 20136 mhpfval 20260 mplbaspropd 20333 ocvfval 20738 isobs 20792 dsmmval 20806 islinds 20881 dmatval 21029 scmatval 21041 cpmat 21245 cldval 21559 mretopd 21628 neifval 21635 ordtval 21725 ordtbas2 21727 ordtcnv 21737 ordtrest2 21740 cnfval 21769 cnpfval 21770 kgenval 22071 xkoval 22123 dfac14 22154 qtopval 22231 qtopval2 22232 hmeofval 22294 elmptrab 22363 fgval 22406 flimval 22499 utopval 22768 ucnval 22813 iscfilu 22824 ispsmet 22841 ismet 22860 isxmet 22861 blfvalps 22920 cncfval 23423 ishtpy 23503 isphtpy 23512 om1val 23561 cfilfval 23794 caufval 23805 cpnfval 24456 uc1pval 24660 mon1pval 24662 dchrval 25737 istrkgl 26171 israg 26410 iseqlg 26580 ttgval 26588 nbgrval 27045 vtxdgfval 27176 vtxdeqd 27186 1egrvtxdg1 27218 umgr2v2evd2 27236 wwlks 27540 wwlksn 27542 wspthsn 27553 wwlksnon 27556 wspthsnon 27557 iswspthsnon 27561 rusgrnumwwlklem 27676 clwwlk 27688 clwwlkn 27731 2clwwlk 28053 numclwlk1lem2 28076 numclwwlkovh0 28078 numclwwlkovq 28080 lnoval 28456 bloval 28485 hmoval 28514 tocycval 30677 prmidlval 30873 ordtprsuni 31061 sigagenval 31298 faeval 31404 ismbfm 31409 carsgval 31460 sitgval 31489 reprval 31780 erdszelem3 32337 erdsze 32346 kur14 32360 iscvm 32403 satf 32497 wlimeq12 33003 fwddifval 33520 poimirlem28 34801 istotbnd 34928 isbnd 34939 rngohomval 35123 rngoisoval 35136 idlval 35172 pridlval 35192 maxidlval 35198 igenval 35220 lshpset 35994 lflset 36075 pats 36301 llnset 36521 lplnset 36545 lvolset 36588 lineset 36754 pmapfval 36772 paddfval 36813 lhpset 37011 ldilfset 37124 ltrnfset 37133 ltrnset 37134 dilfsetN 37168 trnfsetN 37171 trnsetN 37172 diaffval 38046 diafval 38047 dicffval 38190 dochffval 38365 lpolsetN 38498 lcdfval 38604 lcdval 38605 mapdffval 38642 mapdfval 38643 isnacs 39179 mzpclval 39200 k0004val 40378 fourierdlem2 42271 fourierdlem3 42272 etransclem12 42408 etransclem33 42429 caragenval 42652 smflimlem3 42926 fvmptrab 43368 iccpval 43452 ismgmhm 43927 issubmgm 43933 assintopval 44040 rnghmval 44090 isrngisom 44095 dmatALTval 44383 lcoop 44394 lines 44646 rrxlines 44648 spheres 44661 |
Copyright terms: Public domain | W3C validator |