| 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 3451. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
| Ref | Expression |
|---|---|
| rabeqdv.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| rabeqdv | ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rabeqdv.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | rabeq 3451 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 {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: rabeqbidvaOLD 3454 rabsnif 4723 fvmptrabfv 7048 suppvalfng 8192 suppvalfn 8193 suppsnop 8203 fnsuppres 8216 pmvalg 8877 cantnffval 9703 hashbc 14492 elovmpowrd 14596 dfphi2 16811 mrisval 17673 coafval 18109 mndpsuppss 18778 pmtrfval 19468 dprdval 20023 rrgval 20697 lspfval 20971 lsppropd 21017 dsmmbas2 21757 frlmbas 21775 aspval 21893 mvrfval 22001 mhpfval 22142 psdffval 22161 clsfval 23033 ordtrest 23210 ordtrest2lem 23211 ordtrest2 23212 xkoval 23595 xkopt 23663 tsmsval2 24138 cncfval 24914 isphtpy 25013 cfilfval 25298 iscmet 25318 leftval 27902 rightval 27903 ttgval 28883 ttgvalOLD 28884 eengv 28994 isupgr 29101 upgrop 29111 isumgr 29112 upgrun 29135 umgrun 29137 isuspgr 29169 isusgr 29170 isuspgrop 29178 isusgrop 29179 isausgr 29181 ausgrusgrb 29182 usgrstrrepe 29252 lfuhgr1v0e 29271 usgrexi 29458 cusgrsize 29472 1loopgrvd2 29521 wwlksn 29857 wspthsn 29868 iswwlksnon 29873 iswspthsnon 29876 clwwlknonmpo 30108 clwwlknon 30109 clwwlk0on0 30111 rmfsupp2 33242 idlsrgval 33531 rspectopn 33866 zar0ring 33877 ordtprsval 33917 snmlfval 35335 mpstval 35540 pclfvalN 39891 docaffvalN 41123 docafvalN 41124 isprimroot 42094 dvnprodlem1 45961 etransclem11 46260 issmflem 46742 issmfd 46750 cnfsmf 46755 issmflelem 46759 issmfgtlem 46770 issmfgt 46771 issmfled 46772 issmfgtd 46776 issmfgelem 46784 fvmptrabdm 47305 prprspr2 47505 stgrusgra 47926 gpgusgra 48012 assintopmap 48122 dmatALTval 48317 rrxsphere 48669 |
| Copyright terms: Public domain | W3C validator |