| 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 5336 | . 2 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ 𝒫 𝐴) | |
| 2 | 1 | elexd 3504 | 1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 {crab 3436 Vcvv 3480 𝒫 cpw 4600 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-in 3958 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: rabex 5339 rabexd 5340 class2set 5355 exse 5645 elfvmptrab1w 7043 elfvmptrab1 7044 elovmporab 7679 elovmporab1w 7680 elovmporab1 7681 ovmpt3rabdm 7692 elovmpt3rab1 7693 suppval 8187 mpoxopoveq 8244 wdom2d 9620 scottex 9925 tskwe 9990 fin1a2lem12 10451 hashbclem 14491 wrdnfi 14586 wrd2f1tovbij 14999 hashdvds 16812 hashbcval 17040 brric 20504 psrass1lem 21952 psrcom 21988 dmatval 22498 cpmat 22715 fctop 23011 cctop 23013 ppttop 23014 epttop 23016 cldval 23031 neif 23108 neival 23110 neiptoptop 23139 neiptopnei 23140 ordtbaslem 23196 ordtbas2 23199 ordtopn1 23202 ordtopn2 23203 ordtrest2lem 23211 cmpsublem 23407 kgenval 23543 qtopval 23703 kqfval 23731 ordthmeolem 23809 elmptrab 23835 fbssfi 23845 fgval 23878 flimval 23971 flimfnfcls 24036 ptcmplem2 24061 ptcmplem3 24062 tsmsfbas 24136 eltsms 24141 utopval 24241 blvalps 24395 blval 24396 minveclem3b 25462 minveclem3 25463 minveclem4 25466 cutlt 27966 fusgredgfi 29342 nbgrval 29353 cusgrsize 29472 wwlks 29855 wwlksnextbij 29922 clwwlk 30002 vdn0conngrumgrv2 30215 vdgn1frgrv2 30315 frgrwopreglem1 30331 rabfodom 32524 ordtrest2NEWlem 33921 hasheuni 34086 sigaval 34112 ldgenpisyslem1 34164 ddemeas 34237 braew 34243 imambfm 34264 carsgval 34305 iscvm 35264 cvmsval 35271 fwddifval 36163 fnessref 36358 indexa 37740 supex2g 37744 rfovfvfvd 44016 rfovcnvf1od 44017 fsovfvfvd 44024 fsovcnvlem 44026 cnfex 45033 stoweidlem26 46041 stoweidlem31 46046 stoweidlem34 46049 stoweidlem46 46061 stoweidlem59 46074 salexct 46349 caragenval 46508 clnbgrval 47809 dmatALTbas 48318 lcoop 48328 |
| Copyright terms: Public domain | W3C validator |