![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rabeqi | Structured version Visualization version GIF version |
Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3437. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2137, ax-11 2154, ax-12 2171. (Revised by Gino Giotto, 3-Jun-2024.) |
Ref | Expression |
---|---|
rabeqi.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
rabeqi | ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabeqi.1 | . . . 4 ⊢ 𝐴 = 𝐵 | |
2 | 1 | eleq2i 2829 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) |
3 | 2 | anbi1i 624 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)) |
4 | 3 | rabbia2 3409 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∈ wcel 2106 {crab 3406 |
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 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3407 |
This theorem is referenced by: rabrabiOLD 3430 f1ossf1o 7071 hsmex2 10366 iooval2 13294 fzval2 13424 phimullem 16648 pmtrsn 19297 dsmmbas2 21139 qtopres 23045 left1s 27220 right1s 27221 uvtxval 28233 cusgredg 28270 cffldtocusgr 28293 vtxdginducedm1 28389 finsumvtxdg2size 28396 konigsbergiedgw 29090 extwwlkfab 29194 zartopn 32347 satf0 33857 prjspeclsp 40926 k0004val0 42406 smflimlem4 44985 smfliminf 45042 |
Copyright terms: Public domain | W3C validator |