![]() |
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 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | rabeqbidv.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 2 | adantr 481 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
4 | 1, 3 | rabeqbidva 3448 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1541 ∈ wcel 2106 {crab 3432 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 |
This theorem is referenced by: elfvmptrab1w 7011 elfvmptrab1 7012 fvmptrabfv 7016 elovmporab1w 7637 elovmporab1 7638 ovmpt3rab1 7648 suppval 8132 mpoxopoveq 8188 supeq123d 9429 phival 16684 dfphi2 16691 hashbcval 16919 imasval 17441 ismre 17518 mrisval 17558 isacs 17579 monfval 17663 ismon 17664 monpropd 17668 natfval 17881 isnat 17882 initoval 17927 termoval 17928 gsumvalx 18579 gsumpropd 18581 gsumress 18585 ismhm 18651 issubm 18662 issubg 18980 isnsg 19009 isgim 19104 isga 19123 cntzfval 19152 isslw 19442 isirred 20185 dfrhm2 20205 isrim0OLD 20211 isrim0 20213 issubrg 20314 issdrg 20355 abvfval 20377 lssset 20495 islmhm 20589 islmim 20624 islbs 20638 rrgval 20841 ocvfval 21154 isobs 21210 dsmmval 21224 islinds 21299 mplval 21481 mhpfval 21613 mplbaspropd 21692 dmatval 21925 scmatval 21937 cpmat 22142 cldval 22458 mretopd 22527 neifval 22534 ordtval 22624 ordtbas2 22626 ordtcnv 22636 ordtrest2 22639 cnfval 22668 cnpfval 22669 kgenval 22970 xkoval 23022 dfac14 23053 qtopval 23130 qtopval2 23131 hmeofval 23193 elmptrab 23262 fgval 23305 flimval 23398 utopval 23668 ucnval 23713 iscfilu 23724 ispsmet 23741 ismet 23760 isxmet 23761 blfvalps 23820 cncfval 24335 ishtpy 24419 isphtpy 24428 om1val 24477 cfilfval 24712 caufval 24723 cpnfval 25380 uc1pval 25588 mon1pval 25590 dchrval 26666 leftval 27287 rightval 27288 istrkgl 27638 israg 27877 iseqlg 28047 ttgval 28055 ttgvalOLD 28056 nbgrval 28522 vtxdgfval 28653 vtxdeqd 28663 1egrvtxdg1 28695 umgr2v2evd2 28713 wwlks 29018 wwlksn 29020 wspthsn 29031 wwlksnon 29034 wspthsnon 29035 iswspthsnon 29039 rusgrnumwwlklem 29153 clwwlk 29165 clwwlkn 29208 2clwwlk 29529 numclwlk1lem2 29552 numclwwlkovh0 29554 numclwwlkovq 29556 lnoval 29932 bloval 29961 hmoval 29990 mntoval 32087 tocycval 32202 fldgenval 32328 prmidlval 32470 mxidlval 32492 rprmval 32542 minplyval 32666 ordtprsuni 32794 sigagenval 33033 faeval 33139 ismbfm 33144 carsgval 33197 sitgval 33226 reprval 33517 erdszelem3 34079 erdsze 34088 kur14 34102 iscvm 34145 satf 34239 wlimeq12 34685 fwddifval 35028 poimirlem28 36384 istotbnd 36506 isbnd 36517 rngohomval 36701 rngoisoval 36714 idlval 36750 pridlval 36770 maxidlval 36776 igenval 36798 lshpset 37717 lflset 37798 pats 38024 llnset 38245 lplnset 38269 lvolset 38312 lineset 38478 pmapfval 38496 paddfval 38537 lhpset 38735 ldilfset 38848 ltrnfset 38857 ltrnset 38858 dilfsetN 38892 trnfsetN 38895 trnsetN 38896 diaffval 39770 diafval 39771 dicffval 39914 dochffval 40089 lpolsetN 40222 lcdfval 40328 lcdval 40329 mapdffval 40366 mapdfval 40367 prjcrvfval 41219 isnacs 41277 mzpclval 41298 k0004val 42736 fourierdlem2 44662 fourierdlem3 44663 etransclem12 44799 etransclem33 44820 caragenval 45046 smflimlem3 45326 fvmptrab 45836 iccpval 45919 ismgmhm 46389 issubmgm 46395 assintopval 46451 rnghmval 46501 isrngisom 46506 dmatALTval 46793 lcoop 46804 lines 47129 rrxlines 47131 spheres 47144 |
Copyright terms: Public domain | W3C validator |