| 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 480 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
| 4 | 1, 3 | rabeqbidva 3453 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 {crab 3436 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 |
| This theorem is referenced by: elfvmptrab1w 7043 elfvmptrab1 7044 fvmptrabfv 7048 elovmporab1w 7680 elovmporab1 7681 ovmpt3rab1 7691 suppval 8187 mpoxopoveq 8244 supeq123d 9490 phival 16804 dfphi2 16811 hashbcval 17040 imasval 17556 ismre 17633 mrisval 17673 isacs 17694 monfval 17776 ismon 17777 monpropd 17781 natfval 17994 isnat 17995 initoval 18038 termoval 18039 gsumvalx 18689 gsumpropd 18691 gsumress 18695 ismgmhm 18709 issubmgm 18715 ismhm 18798 issubm 18816 issubg 19144 isnsg 19173 isgim 19280 isga 19309 cntzfval 19338 isslw 19626 isirred 20419 rnghmval 20440 isrngim 20445 dfrhm2 20474 isrim0OLD 20481 isrim0 20483 issubrng 20547 issubrg 20571 rrgval 20697 issdrg 20789 abvfval 20811 lssset 20931 islmhm 21026 islmim 21061 islbs 21075 ocvfval 21684 isobs 21740 dsmmval 21754 islinds 21829 mplval 22009 mhpfval 22142 mplbaspropd 22238 dmatval 22498 scmatval 22510 cpmat 22715 cldval 23031 mretopd 23100 neifval 23107 ordtval 23197 ordtbas2 23199 ordtcnv 23209 ordtrest2 23212 cnfval 23241 cnpfval 23242 kgenval 23543 xkoval 23595 dfac14 23626 qtopval 23703 qtopval2 23704 hmeofval 23766 elmptrab 23835 fgval 23878 flimval 23971 utopval 24241 ucnval 24286 iscfilu 24297 ispsmet 24314 ismet 24333 isxmet 24334 blfvalps 24393 cncfval 24914 ishtpy 25004 isphtpy 25013 om1val 25063 cfilfval 25298 caufval 25309 cpnfval 25968 uc1pval 26179 mon1pval 26181 dchrval 27278 leftval 27902 rightval 27903 istrkgl 28466 israg 28705 iseqlg 28875 ttgval 28883 ttgvalOLD 28884 nbgrval 29353 vtxdgfval 29485 vtxdeqd 29495 1egrvtxdg1 29527 umgr2v2evd2 29545 wwlks 29855 wwlksn 29857 wspthsn 29868 wwlksnon 29871 wspthsnon 29872 iswspthsnon 29876 rusgrnumwwlklem 29990 clwwlk 30002 clwwlkn 30045 2clwwlk 30366 numclwlk1lem2 30389 numclwwlkovh0 30391 numclwwlkovq 30393 lnoval 30771 bloval 30800 hmoval 30829 mntoval 32972 tocycval 33128 fldgenval 33314 prmidlval 33465 mxidlval 33489 rprmval 33544 minplyval 33748 ordtprsuni 33918 sigagenval 34141 faeval 34247 ismbfm 34252 carsgval 34305 sitgval 34334 reprval 34625 erdszelem3 35198 erdsze 35207 kur14 35221 iscvm 35264 satf 35358 wlimeq12 35820 fwddifval 36163 poimirlem28 37655 istotbnd 37776 isbnd 37787 rngohomval 37971 rngoisoval 37984 idlval 38020 pridlval 38040 maxidlval 38046 igenval 38068 lshpset 38979 lflset 39060 pats 39286 llnset 39507 lplnset 39531 lvolset 39574 lineset 39740 pmapfval 39758 paddfval 39799 lhpset 39997 ldilfset 40110 ltrnfset 40119 ltrnset 40120 dilfsetN 40154 trnfsetN 40157 trnsetN 40158 diaffval 41032 diafval 41033 dicffval 41176 dochffval 41351 lpolsetN 41484 lcdfval 41590 lcdval 41591 mapdffval 41628 mapdfval 41629 prjcrvfval 42641 isnacs 42715 mzpclval 42736 k0004val 44163 dvnprodlem1 45961 fourierdlem2 46124 fourierdlem3 46125 etransclem12 46261 etransclem33 46282 caragenval 46508 smflimlem3 46788 fvmptrab 47304 iccpval 47402 clnbgrval 47809 isisubgr 47848 grtri 47907 stgrfv 47920 gpgov 48001 assintopval 48121 dmatALTval 48317 lcoop 48328 lines 48652 rrxlines 48654 spheres 48667 |
| Copyright terms: Public domain | W3C validator |