| 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 5310 | . 2 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ 𝒫 𝐴) | |
| 2 | 1 | elexd 3481 | 1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∈ wcel 2146 {crab 3419 Vcvv 3458 𝒫 cpw 4565 |
| 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 2738 ax-sep 5260 |
| 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 2745 df-cleq 2758 df-clel 2841 df-rab 3420 df-v 3460 df-in 3915 df-ss 3925 df-pw 4567 |
| This theorem is used by: rabex 5312 rabexd 5313 class2set 5328 exse 5624 elfvmptrab1w 7021 elfvmptrab1 7022 elovmporab 7662 elovmporab1w 7663 elovmporab1 7664 ovmpt3rabdm 7675 elovmpt3rab1 7676 suppval 8160 mpoxopoveq 8217 wdom2d 9544 scottex 9864 scottexOLD 9865 tskwe 9947 fin1a2lem12 10405 hashbclem 14500 wrdnfi 14596 wrd2f1tovbij 15008 hashdvds 16844 hashbcval 17072 brric 20608 psrass1lem 22098 psrcom 22132 dmatval 22664 cpmat 22881 fctop 23176 cctop 23178 ppttop 23179 epttop 23181 cldval 23195 neif 23272 neival 23274 neiptoptop 23303 neiptopnei 23304 ordtbaslem 23360 ordtbas2 23363 ordtopn1 23366 ordtopn2 23367 ordtrest2lem 23375 cmpsublem 23571 kgenval 23707 qtopval 23867 kqfval 23895 ordthmeolem 23973 elmptrab 23999 fbssfi 24009 fgval 24042 flimval 24135 flimfnfcls 24200 ptcmplem2 24225 ptcmplem3 24226 tsmsfbas 24300 eltsms 24305 utopval 24404 blvalps 24557 blval 24558 minveclem3b 25602 minveclem3 25603 minveclem4 25606 cutlt 28140 fusgredgfi 29690 nbgrval 29701 cusgrsize 29819 wwlks 30199 wwlksnextbij 30266 clwwlk 30349 vdn0conngrumgrv2 30562 vdgn1frgrv2 30662 frgrwopreglem1 30678 rabfodom 32866 ordtrest2NEWlem 34325 hasheuni 34488 sigaval 34514 ldgenpisyslem1 34566 ddemeas 34639 braew 34645 imambfm 34665 carsgval 34706 iscvm 35763 cvmsval 35770 fwddifval 36666 fnessref 36900 indexa 38416 supex2g 38420 rfovfvfvd 44761 rfovcnvf1od 44762 fsovfvfvd 44769 fsovcnvlem 44771 cnfex 45780 stoweidlem26 46772 stoweidlem31 46777 stoweidlem34 46780 stoweidlem46 46792 stoweidlem59 46805 salexct 47080 caragenval 47239 clnbgrval 48619 dmatALTbas 49213 lcoop 49223 |
| Copyright terms: Public domain | W3C validator |