Theorem rabex2 5330

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 5329	. 2 ⊢ (𝐴 ∈ V → 𝐵 ∈ V)
5	1, 4	ax-mp 5	1 ⊢ 𝐵 ∈ V

Syntax hints:   = wceq 1534   ∈ wcel 2099  {crab 3427  Vcvv 3469

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 2698  ax-sep 5293

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-in 3951  df-ss 3961

This theorem is referenced by:  rab2ex  5331  mapfien2  9426  cantnffval  9680  nqex  10940  gsumvalx  18629  psgnfval  19448  odval  19482  sylow1lem2  19547  sylow3lem6  19580  ablfaclem1  20035  psrass1lemOLD  21867  psrass1lem  21870  psrbas  21871  psrelbas  21872  psrmulfval  21879  psrmulcllem  21881  psrvscaval  21886  psr0cl  21888  psr0lid  21889  psrnegcl  21890  psrlinv  21891  psr1cl  21897  psrlidm  21898  psrdi  21901  psrdir  21902  psrass23l  21903  psrcom  21904  psrass23  21905  mvrval  21917  mplsubglem  21934  mpllsslem  21935  mplsubrglem  21939  mplvscaval  21951  mplmon  21966  mplmonmul  21967  mplcoe1  21968  ltbval  21974  mplmon2  21998  evlslem2  22018  evlslem3  22019  evlslem1  22021  psdval  22076  rrxmet  25329  mdegldg  25995  lgamgulmlem5  26958  lgamgulmlem6  26959  lgamgulm2  26961  lgamcvglem  26965  upgrres1lem1  29115  frgrwopreg1  30121  dlwwlknondlwlknonen  30169  nsgmgc  33116  nsgqusf1o  33120  eulerpartlem1  33977  eulerpartlemt  33981  eulerpartgbij  33982  ballotlemoex  34095  satffunlem2lem2  35006  mapdunirnN  41112  mplmapghm  41761  evlsvvvallem2  41767  selvvvval  41790  evlsmhpvvval  41800  pwfi2en  42493  smfresal  46148  oddiadd  47208  2zrngadd  47277  2zrngmul  47285