Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rabeq | Structured version Visualization version GIF version |
Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2136, ax-11 2151, ax-12 2167. (Revised by Gino Giotto, 20-Aug-2023.) |
Ref | Expression |
---|---|
rabeq | ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 2901 | . . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | 1 | anbi1d 629 | . 2 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))) |
3 | 2 | rabbidva2 3477 | 1 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 {crab 3142 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-rab 3147 |
This theorem is referenced by: rabeqdv 3485 difeq1 4091 ineq1 4180 ifeq1 4469 ifeq2 4470 elfvmptrab 6789 supp0 7826 supeq2 8901 oieq2 8966 scott0 9304 mrcfval 16869 ipoval 17754 psgnfval 18559 lsppropd 19721 psrval 20072 ltbval 20182 opsrval 20185 dsmmelbas 20813 m1detdiag 21136 isptfin 22054 islocfin 22055 kqval 22264 incistruhgr 26792 uvtx0 27104 vtxdg0e 27184 1hevtxdg1 27216 hashecclwwlkn1 27784 umgrhashecclwwlk 27785 ordtrestNEW 31064 ordtrest2NEWlem 31065 omsval 31451 orrvcval4 31622 orrvcoel 31623 orrvccel 31624 funray 33499 fvray 33500 itg2addnclem2 34826 cntotbnd 34957 lcfr 38603 hlhilocv 38975 pellfundval 39357 elmnc 39616 rgspnval 39648 rfovd 40227 fsovd 40234 fsovcnvlem 40239 ntrneibex 40303 dvnprodlem1 42111 dvnprodlem2 42112 dvnprodlem3 42113 dvnprod 42114 fvmptrab 43372 rmsuppss 44316 mndpsuppss 44317 scmsuppss 44318 dmatALTbas 44354 |
Copyright terms: Public domain | W3C validator |