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 5257 | . 2 ⊢ (𝐴 ∈ V → 𝐵 ∈ V) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ 𝐵 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∈ wcel 2106 {crab 3068 Vcvv 3432 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-sep 5223 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-in 3894 df-ss 3904 |
This theorem is referenced by: rab2ex 5259 mapfien2 9168 cantnffval 9421 nqex 10679 gsumvalx 18360 psgnfval 19108 odval 19142 sylow1lem2 19204 sylow3lem6 19237 ablfaclem1 19688 psrass1lemOLD 21143 psrass1lem 21146 psrbas 21147 psrelbas 21148 psrmulfval 21154 psrmulcllem 21156 psrvscaval 21161 psr0cl 21163 psr0lid 21164 psrnegcl 21165 psrlinv 21166 psr1cl 21171 psrlidm 21172 psrdi 21175 psrdir 21176 psrass23l 21177 psrcom 21178 psrass23 21179 mvrval 21190 mplsubglem 21205 mpllsslem 21206 mplsubrglem 21210 mplvscaval 21220 mplmon 21236 mplmonmul 21237 mplcoe1 21238 ltbval 21244 mplmon2 21269 evlslem2 21289 evlslem3 21290 evlslem1 21292 rrxmet 24572 mdegldg 25231 lgamgulmlem5 26182 lgamgulmlem6 26183 lgamgulm2 26185 lgamcvglem 26189 upgrres1lem1 27676 frgrwopreg1 28682 dlwwlknondlwlknonen 28730 nsgmgc 31597 nsgqusf1o 31601 eulerpartlem1 32334 eulerpartlemt 32338 eulerpartgbij 32339 ballotlemoex 32452 satffunlem2lem2 33368 mapdunirnN 39664 pwfi2en 40922 smfresal 44322 oddiadd 45368 2zrngadd 45495 2zrngmul 45503 |
Copyright terms: Public domain | W3C validator |