![]() |
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 5294 | . 2 ⊢ (𝐴 ∈ V → 𝐵 ∈ V) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ 𝐵 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∈ wcel 2107 {crab 3406 Vcvv 3447 |
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 5260 |
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 3407 df-v 3449 df-in 3921 df-ss 3931 |
This theorem is referenced by: rab2ex 5296 mapfien2 9353 cantnffval 9607 nqex 10867 gsumvalx 18539 psgnfval 19290 odval 19324 sylow1lem2 19389 sylow3lem6 19422 ablfaclem1 19872 psrass1lemOLD 21365 psrass1lem 21368 psrbas 21369 psrelbas 21370 psrmulfval 21376 psrmulcllem 21378 psrvscaval 21383 psr0cl 21385 psr0lid 21386 psrnegcl 21387 psrlinv 21388 psr1cl 21394 psrlidm 21395 psrdi 21398 psrdir 21399 psrass23l 21400 psrcom 21401 psrass23 21402 mvrval 21413 mplsubglem 21428 mpllsslem 21429 mplsubrglem 21433 mplvscaval 21443 mplmon 21459 mplmonmul 21460 mplcoe1 21461 ltbval 21467 mplmon2 21492 evlslem2 21512 evlslem3 21513 evlslem1 21515 rrxmet 24795 mdegldg 25454 lgamgulmlem5 26405 lgamgulmlem6 26406 lgamgulm2 26408 lgamcvglem 26412 upgrres1lem1 28306 frgrwopreg1 29311 dlwwlknondlwlknonen 29359 nsgmgc 32245 nsgqusf1o 32249 eulerpartlem1 33031 eulerpartlemt 33035 eulerpartgbij 33036 ballotlemoex 33149 satffunlem2lem2 34064 mapdunirnN 40163 pwfi2en 41471 smfresal 45119 oddiadd 46198 2zrngadd 46325 2zrngmul 46333 |
Copyright terms: Public domain | W3C validator |