![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rabeqdv | Structured version Visualization version GIF version |
Description: Equality of restricted class abstractions. Deduction form of rabeq 3442. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
Ref | Expression |
---|---|
rabeqdv.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
rabeqdv | ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabeqdv.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | rabeq 3442 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 {crab 3428 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-rab 3429 |
This theorem is referenced by: rabeqbidva 3444 rabsnif 4724 fvmptrabfv 7032 suppvalfng 8167 suppvalfn 8168 suppsnop 8177 fnsuppres 8190 pmvalg 8850 cantnffval 9681 hashbc 14439 elovmpowrd 14535 dfphi2 16737 mrisval 17604 coafval 18047 pmtrfval 19399 dprdval 19954 lspfval 20851 lsppropd 20897 rrgval 21228 dsmmbas2 21665 frlmbas 21683 aspval 21800 mvrfval 21917 mhpfval 22057 psdffval 22075 clsfval 22923 ordtrest 23100 ordtrest2lem 23101 ordtrest2 23102 xkoval 23485 xkopt 23553 tsmsval2 24028 cncfval 24802 isphtpy 24901 cfilfval 25186 iscmet 25206 leftval 27784 rightval 27785 ttgval 28673 ttgvalOLD 28674 eengv 28784 isupgr 28891 upgrop 28901 isumgr 28902 upgrun 28925 umgrun 28927 isuspgr 28959 isusgr 28960 isuspgrop 28968 isusgrop 28969 isausgr 28971 ausgrusgrb 28972 usgrstrrepe 29042 lfuhgr1v0e 29061 usgrexmpl 29070 usgrexi 29248 cusgrsize 29262 1loopgrvd2 29311 wwlksn 29642 wspthsn 29653 iswwlksnon 29658 iswspthsnon 29661 clwwlknonmpo 29893 clwwlknon 29894 clwwlk0on0 29896 rmfsupp2 32941 idlsrgval 33209 rspectopn 33463 zar0ring 33474 ordtprsval 33514 snmlfval 34935 mpstval 35140 pclfvalN 39357 docaffvalN 40589 docafvalN 40590 isprimroot 41559 etransclem11 45624 issmflem 46106 issmfd 46114 cnfsmf 46119 issmflelem 46123 issmfgtlem 46134 issmfgt 46135 issmfled 46136 issmfgtd 46140 issmfgelem 46148 fvmptrabdm 46664 prprspr2 46849 assintopmap 47259 mndpsuppss 47426 dmatALTval 47459 rrxsphere 47812 |
Copyright terms: Public domain | W3C validator |