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 3967 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 | |
2 | ssexg 5188 | . 2 ⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) | |
3 | 1, 2 | mpan 690 | 1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2113 {crab 3057 Vcvv 3397 ⊆ wss 3841 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 ax-sep 5164 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-rab 3062 df-v 3399 df-in 3848 df-ss 3858 |
This theorem is referenced by: rabex 5197 rabexd 5198 class2set 5217 exse 5483 elfvmptrab1w 6795 elfvmptrab1 6796 elovmporab 7401 elovmporab1w 7402 elovmporab1 7403 ovmpt3rabdm 7414 elovmpt3rab1 7415 suppval 7851 mpoxopoveq 7907 wdom2d 9110 scottex 9380 tskwe 9445 fin1a2lem12 9904 hashbclem 13895 wrdnfi 13982 wrd2f1tovbij 14406 hashdvds 16205 hashbcval 16431 brric 19611 psrass1lemOLD 20746 psrass1lem 20749 psrcom 20781 dmatval 21236 cpmat 21453 fctop 21748 cctop 21750 ppttop 21751 epttop 21753 cldval 21767 neif 21844 neival 21846 neiptoptop 21875 neiptopnei 21876 ordtbaslem 21932 ordtbas2 21935 ordtopn1 21938 ordtopn2 21939 ordtrest2lem 21947 cmpsublem 22143 kgenval 22279 qtopval 22439 kqfval 22467 ordthmeolem 22545 elmptrab 22571 fbssfi 22581 fgval 22614 flimval 22707 flimfnfcls 22772 ptcmplem2 22797 ptcmplem3 22798 tsmsfbas 22872 eltsms 22877 utopval 22977 blvalps 23131 blval 23132 minveclem3b 24173 minveclem3 24174 minveclem4 24177 fusgredgfi 27259 nbgrval 27270 cusgrsize 27388 wwlks 27765 wwlksnextbij 27832 clwwlk 27912 vdn0conngrumgrv2 28125 vdgn1frgrv2 28225 frgrwopreglem1 28241 rabfodom 30417 ordtrest2NEWlem 31436 hasheuni 31615 sigaval 31641 ldgenpisyslem1 31693 ddemeas 31766 braew 31772 imambfm 31791 carsgval 31832 iscvm 32784 cvmsval 32791 fwddifval 34094 fnessref 34176 indexa 35503 supex2g 35507 rfovfvfvd 41141 rfovcnvf1od 41142 fsovfvfvd 41149 fsovcnvlem 41151 cnfex 42093 stoweidlem26 43093 stoweidlem31 43098 stoweidlem34 43101 stoweidlem46 43113 stoweidlem59 43126 salexct 43399 caragenval 43557 dmatALTbas 45260 lcoop 45270 |
Copyright terms: Public domain | W3C validator |