| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rabexg | Structured version Visualization version GIF version | ||
| Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.) (Proof shortened by BJ, 24-Jul-2025.) |
| Ref | Expression |
|---|---|
| rabexg | ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rabelpw 5309 | . 2 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ 𝒫 𝐴) | |
| 2 | 1 | elexd 3480 | 1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∈ wcel 2146 {crab 3418 Vcvv 3457 𝒫 cpw 4564 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-ext 2737 ax-sep 5259 |
| This proof depends on definitions: df-bi 210 df-an 402 df-3an 1105 df-tru 1573 df-ex 1813 df-sb 2100 df-clab 2744 df-cleq 2757 df-clel 2840 df-rab 3419 df-v 3459 df-in 3913 df-ss 3923 df-pw 4566 |
| This theorem is used by: rabex 5311 rabexd 5312 class2set 5327 exse 5623 elfvmptrab1w 7021 elfvmptrab1 7022 elovmporab 7666 elovmporab1w 7667 elovmporab1 7668 ovmpt3rabdm 7679 elovmpt3rab1 7680 suppval 8164 mpoxopoveq 8221 wdom2d 9549 scottex 9869 scottexOLD 9870 tskwe 9952 fin1a2lem12 10410 hashbclem 14507 wrdnfi 14603 wrd2f1tovbij 15021 hashdvds 16856 hashbcval 17084 brric 20643 psrass1lem 22133 psrcom 22167 dmatval 22699 cpmat 22916 fctop 23211 cctop 23213 ppttop 23214 epttop 23216 cldval 23230 neif 23307 neival 23309 neiptoptop 23338 neiptopnei 23339 ordtbaslem 23395 ordtbas2 23398 ordtopn1 23401 ordtopn2 23402 ordtrest2lem 23410 cmpsublem 23606 kgenval 23743 qtopval 23903 kqfval 23931 ordthmeolem 24009 elmptrab 24035 fbssfi 24045 fgval 24078 flimval 24171 flimfnfcls 24236 ptcmplem2 24261 ptcmplem3 24262 tsmsfbas 24336 eltsms 24341 utopval 24440 blvalps 24593 blval 24594 minveclem3b 25638 minveclem3 25639 minveclem4 25642 cutlt 28176 fusgredgfi 29733 nbgrval 29744 cusgrsize 29862 wwlks 30251 wwlksnextbij 30318 clwwlk 30401 vdn0conngrumgrv2 30618 vdgn1frgrv2 30718 frgrwopreglem1 30734 rabfodom 32922 ordtrest2NEWlem 34376 hasheuni 34539 sigaval 34565 ldgenpisyslem1 34618 ddemeas 34691 braew 34697 imambfm 34717 carsgval 34758 iscvm 35788 cvmsval 35795 fwddifval 36691 fnessref 36925 indexa 38442 supex2g 38446 rfovfvfvd 44787 rfovcnvf1od 44788 fsovfvfvd 44795 fsovcnvlem 44797 cnfex 45806 stoweidlem26 46798 stoweidlem31 46803 stoweidlem34 46806 stoweidlem46 46818 stoweidlem59 46831 salexct 47106 caragenval 47265 clnbgrval 48645 dmatALTbas 49238 lcoop 49248 |
| Copyright terms: Public domain | W3C validator |