rabex2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rabex2		Structured version Visualization version GIF version

Theorem rabex2 5336

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.)

**Hypotheses**
Ref	Expression
rabex2.1	⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}
rabex2.2	⊢ 𝐴 ∈ V

**Assertion**
Ref	Expression
rabex2	⊢ 𝐵 ∈ V

Distinct variable group: 𝑥,𝐴 Allowed substitution hints: 𝜓(𝑥) 𝐵(𝑥)

**Proof of Theorem rabex2**
Step	Hyp	Ref	Expression
1		rabex2.2	. 2 ⊢ 𝐴 ∈ V
2		rabex2.1	. . 3 ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}
3		id 22	. . 3 ⊢ (𝐴 ∈ V → 𝐴 ∈ V)
4	2, 3	rabexd 5335	. 2 ⊢ (𝐴 ∈ V → 𝐵 ∈ V)
5	1, 4	ax-mp 5	1 ⊢ 𝐵 ∈ V

Colors of variables: wff setvar class

Syntax hints: = wceq 1534 ∈ wcel 2099 {crab 3429 Vcvv 3471

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-sep 5299

This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-rab 3430 df-v 3473 df-in 3954 df-ss 3964

This theorem is referenced by: rab2ex 5337 mapfien2 9433 cantnffval 9687 nqex 10947 gsumvalx 18636 psgnfval 19455 odval 19489 sylow1lem2 19554 sylow3lem6 19587 ablfaclem1 20042 psrass1lemOLD 21874 psrass1lem 21877 psrbas 21878 psrelbas 21879 psrmulfval 21886 psrmulcllem 21888 psrvscaval 21893 psr0cl 21895 psr0lid 21896 psrnegcl 21897 psrlinv 21898 psr1cl 21904 psrlidm 21905 psrdi 21908 psrdir 21909 psrass23l 21910 psrcom 21911 psrass23 21912 mvrval 21924 mplsubglem 21941 mpllsslem 21942 mplsubrglem 21946 mplvscaval 21958 mplmon 21973 mplmonmul 21974 mplcoe1 21975 ltbval 21981 mplmon2 22005 evlslem2 22025 evlslem3 22026 evlslem1 22028 psdval 22083 rrxmet 25349 mdegldg 26015 lgamgulmlem5 26978 lgamgulmlem6 26979 lgamgulm2 26981 lgamcvglem 26985 upgrres1lem1 29135 frgrwopreg1 30141 dlwwlknondlwlknonen 30189 nsgmgc 33135 nsgqusf1o 33139 eulerpartlem1 33987 eulerpartlemt 33991 eulerpartgbij 33992 ballotlemoex 34105 satffunlem2lem2 35016 mapdunirnN 41123 mplmapghm 41789 evlsvvvallem2 41795 selvvvval 41818 evlsmhpvvval 41828 pwfi2en 42521 smfresal 46176 oddiadd 47236 2zrngadd 47305 2zrngmul 47313

	
		OSZAR »