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 5211 | . 2 ⊢ (𝐴 ∈ V → 𝐵 ∈ V) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ 𝐵 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∈ wcel 2114 {crab 3058 Vcvv 3400 |
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 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 ax-sep 5177 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-rab 3063 df-v 3402 df-in 3860 df-ss 3870 |
This theorem is referenced by: rab2ex 5213 mapfien2 8959 cantnffval 9212 nqex 10436 gsumvalx 18015 psgnfval 18759 odval 18793 sylow1lem2 18855 sylow3lem6 18888 ablfaclem1 19339 psrass1lemOLD 20766 psrass1lem 20769 psrbas 20770 psrelbas 20771 psrmulfval 20777 psrmulcllem 20779 psrvscaval 20784 psr0cl 20786 psr0lid 20787 psrnegcl 20788 psrlinv 20789 psr1cl 20794 psrlidm 20795 psrdi 20798 psrdir 20799 psrass23l 20800 psrcom 20801 psrass23 20802 mvrval 20813 mplsubglem 20828 mpllsslem 20829 mplsubrglem 20833 mplvscaval 20843 mplmon 20859 mplmonmul 20860 mplcoe1 20861 ltbval 20867 mplmon2 20886 evlslem2 20906 evlslem3 20907 evlslem1 20909 rrxmet 24173 mdegldg 24832 lgamgulmlem5 25783 lgamgulmlem6 25784 lgamgulm2 25786 lgamcvglem 25790 upgrres1lem1 27264 frgrwopreg1 28268 dlwwlknondlwlknonen 28316 nsgmgc 31182 nsgqusf1o 31186 eulerpartlem1 31917 eulerpartlemt 31921 eulerpartgbij 31922 ballotlemoex 32035 satffunlem2lem2 32952 mapdunirnN 39320 pwfi2en 40535 smfresal 43902 oddiadd 44950 2zrngadd 45077 2zrngmul 45085 |
Copyright terms: Public domain | W3C validator |