Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rabex2 | Structured version Visualization version GIF version |
Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.) |
Ref | Expression |
---|---|
rabex2.1 | ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓} |
rabex2.2 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
rabex2 | ⊢ 𝐵 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabex2.2 | . 2 ⊢ 𝐴 ∈ V | |
2 | rabex2.1 | . . 3 ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓} | |
3 | id 22 | . . 3 ⊢ (𝐴 ∈ V → 𝐴 ∈ V) | |
4 | 2, 3 | rabexd 5228 | . 2 ⊢ (𝐴 ∈ V → 𝐵 ∈ V) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ 𝐵 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∈ wcel 2110 {crab 3142 Vcvv 3494 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-in 3942 df-ss 3951 |
This theorem is referenced by: rab2ex 5230 mapfien2 8866 cantnffval 9120 nqex 10339 gsumvalx 17880 psgnfval 18622 odval 18656 sylow1lem2 18718 sylow3lem6 18751 ablfaclem1 19201 psrass1lem 20151 psrbas 20152 psrelbas 20153 psrmulfval 20159 psrmulcllem 20161 psrvscaval 20166 psr0cl 20168 psr0lid 20169 psrnegcl 20170 psrlinv 20171 psr1cl 20176 psrlidm 20177 psrdi 20180 psrdir 20181 psrass23l 20182 psrcom 20183 psrass23 20184 mvrval 20195 mplsubglem 20208 mpllsslem 20209 mplsubrglem 20213 mplvscaval 20222 mplmon 20238 mplmonmul 20239 mplcoe1 20240 ltbval 20246 opsrtoslem2 20259 mplmon2 20267 evlslem2 20286 evlslem3 20287 evlslem1 20289 rrxmet 24005 mdegldg 24654 lgamgulmlem5 25604 lgamgulmlem6 25605 lgamgulm2 25607 lgamcvglem 25611 upgrres1lem1 27085 frgrwopreg1 28091 dlwwlknondlwlknonen 28139 eulerpartlem1 31620 eulerpartlemt 31624 eulerpartgbij 31625 ballotlemoex 31738 satffunlem2lem2 32648 mapdunirnN 38780 pwfi2en 39690 smfresal 43057 oddiadd 44075 2zrngadd 44202 2zrngmul 44210 |
Copyright terms: Public domain | W3C validator |