![]() |
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 3389. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
Ref | Expression |
---|---|
rabeqdv.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
rabeqdv | ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabeqdv.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | rabeq 3389 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 {crab 3094 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rab 3099 |
This theorem is referenced by: rabeqbidv 3392 rabeqbidva 3393 rabsnif 4490 fvmptrabfv 6571 suppvalfn 7583 fnsuppres 7604 pmvalg 8151 cantnffval 8857 hashbc 13551 elovmpt2wrd 13648 dfphi2 15883 mrisval 16676 coafval 17099 pmtrfval 18253 dprdval 18789 cncfval 23099 eengv 26328 incistruhgr 26427 isupgr 26432 upgrop 26442 isumgr 26443 upgrun 26466 umgrun 26468 isuspgr 26501 isusgr 26502 isuspgrop 26510 isusgrop 26511 isausgr 26513 ausgrusgrb 26514 usgrstrrepe 26582 lfuhgr1v0e 26601 usgrexmpl 26610 usgrexi 26789 cusgrsize 26802 1loopgrvd2 26851 wwlksn 27186 wspthsn 27197 iswwlksnon 27202 iswspthsnon 27205 clwwlknonmpt2 27491 clwwlknon 27492 clwwlk0on0 27494 mpstval 32031 pclfvalN 36045 etransclem11 41393 fvmptrabdm 42338 prprspr2 42461 rrxsphere 43488 |
Copyright terms: Public domain | W3C validator |