![]() |
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.) |
Ref | Expression |
---|---|
rabexg | ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssrab2 4075 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 | |
2 | ssexg 5319 | . 2 ⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) | |
3 | 1, 2 | mpan 689 | 1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 {crab 3433 Vcvv 3475 ⊆ wss 3946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5295 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-in 3953 df-ss 3963 |
This theorem is referenced by: rabex 5328 rabexd 5329 class2set 5349 exse 5635 elfvmptrab1w 7013 elfvmptrab1 7014 elovmporab 7639 elovmporab1w 7640 elovmporab1 7641 ovmpt3rabdm 7652 elovmpt3rab1 7653 suppval 8135 mpoxopoveq 8191 wdom2d 9562 scottex 9867 tskwe 9932 fin1a2lem12 10393 hashbclem 14398 wrdnfi 14485 wrd2f1tovbij 14898 hashdvds 16695 hashbcval 16922 brric 20261 psrass1lemOLD 21464 psrass1lem 21467 psrcom 21500 dmatval 21963 cpmat 22180 fctop 22476 cctop 22478 ppttop 22479 epttop 22481 cldval 22496 neif 22573 neival 22575 neiptoptop 22604 neiptopnei 22605 ordtbaslem 22661 ordtbas2 22664 ordtopn1 22667 ordtopn2 22668 ordtrest2lem 22676 cmpsublem 22872 kgenval 23008 qtopval 23168 kqfval 23196 ordthmeolem 23274 elmptrab 23300 fbssfi 23310 fgval 23343 flimval 23436 flimfnfcls 23501 ptcmplem2 23526 ptcmplem3 23527 tsmsfbas 23601 eltsms 23606 utopval 23706 blvalps 23860 blval 23861 minveclem3b 24914 minveclem3 24915 minveclem4 24918 cutlt 27386 fusgredgfi 28549 nbgrval 28560 cusgrsize 28678 wwlks 29056 wwlksnextbij 29123 clwwlk 29203 vdn0conngrumgrv2 29416 vdgn1frgrv2 29516 frgrwopreglem1 29532 rabfodom 31708 ordtrest2NEWlem 32833 hasheuni 33014 sigaval 33040 ldgenpisyslem1 33092 ddemeas 33165 braew 33171 imambfm 33192 carsgval 33233 iscvm 34181 cvmsval 34188 fwddifval 35065 fnessref 35147 indexa 36507 supex2g 36511 rfovfvfvd 42625 rfovcnvf1od 42626 fsovfvfvd 42633 fsovcnvlem 42635 cnfex 43583 stoweidlem26 44615 stoweidlem31 44620 stoweidlem34 44623 stoweidlem46 44635 stoweidlem59 44648 salexct 44923 caragenval 45082 dmatALTbas 46922 lcoop 46932 |
Copyright terms: Public domain | W3C validator |