| 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 5340 | . 2 ⊢ (𝐴 ∈ V → 𝐵 ∈ V) |
| 5 | 1, 4 | ax-mp 5 | 1 ⊢ 𝐵 ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∈ wcel 2108 {crab 3436 Vcvv 3480 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-in 3958 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: rab2ex 5342 mapfien2 9449 cantnffval 9703 nqex 10963 gsumvalx 18689 psgnfval 19518 odval 19552 sylow1lem2 19617 sylow3lem6 19650 ablfaclem1 20105 psrass1lem 21952 psrbas 21953 psrelbas 21954 psrmulfval 21963 psrmulcllem 21965 psrvscaval 21970 psr0cl 21972 psr0lid 21973 psrnegcl 21974 psrlinv 21975 psr1cl 21981 psrlidm 21982 psrdi 21985 psrdir 21986 psrass23l 21987 psrcom 21988 psrass23 21989 mvrval 22002 mplsubglem 22019 mpllsslem 22020 mplsubrglem 22024 mplvscaval 22036 mplmon 22053 mplmonmul 22054 mplcoe1 22055 ltbval 22061 mplmon2 22085 evlslem2 22103 evlslem3 22104 evlslem1 22106 psdval 22163 rrxmet 25442 mdegldg 26105 lgamgulmlem5 27076 lgamgulmlem6 27077 lgamgulm2 27079 lgamcvglem 27083 upgrres1lem1 29326 frgrwopreg1 30337 dlwwlknondlwlknonen 30385 nsgmgc 33440 nsgqusf1o 33444 ssdifidl 33485 eulerpartlem1 34369 eulerpartlemt 34373 eulerpartgbij 34374 ballotlemoex 34488 satffunlem2lem2 35411 mapdunirnN 41652 mplmapghm 42566 evlsvvvallem2 42572 selvvvval 42595 evlsmhpvvval 42605 pwfi2en 43109 smfresal 46803 oddiadd 48090 2zrngadd 48159 2zrngmul 48167 |
| Copyright terms: Public domain | W3C validator |