Theorem rabexd 5296

Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5297. (Contributed by AV, 16-Jul-2019.)

Hypotheses

Ref	Expression
rabexd.1	⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}
rabexd.2	⊢ (𝜑 → 𝐴 ∈ 𝑉)

Assertion

Ref	Expression
rabexd	⊢ (𝜑 → 𝐵 ∈ V)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem rabexd

Step	Hyp	Ref	Expression
1		rabexd.1	. 2 ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}
2		rabexd.2	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		rabexg 5293	. . 3 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V)
4	2, 3	syl 17	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V)
5	1, 4	eqeltrid 2866	1 ⊢ (𝜑 → 𝐵 ∈ V)

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  {crab 3414  Vcvv 3454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1100  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-in 3911  df-ss 3921  df-pw 4557

This theorem is referenced by:  rabex2  5297  zorn2lem1  10453  sylow2a  19659  psrascl  22027  evlslem6  22131  evlsvvval  22143  mhmcompl  22171  mhmcoaddmpl  22173  mhpaddcl  22213  mretopd  23149  plngval  28981  cusgrexilem1  29637  vtxdgf  29669  mntoval  33157  tocycval  33285  fxpval  33342  prmidlval  33620  selvply1rhmlemb  33813  extvfvcl  33830  isprimroot  42707  primrootsunit1  42711  unitscyglem1  42809  evlsbagval  43165  mhpind  43173  stoweidlem35  46606  stoweidlem50  46621  stoweidlem57  46628  stoweidlem59  46630  subsaliuncllem  46928  subsaliuncl  46929  smflimlem1  47342  smflimlem2  47343  smflimlem3  47344  smflimlem6  47347  smfrec  47360  smfpimcclem  47378  smfsuplem1  47382  smfinflem  47388  smflimsuplem1  47391  smflimsuplem2  47392  smflimsuplem3  47393  smflimsuplem4  47394  smflimsuplem5  47395  smflimsuplem7  47397  fvmptrab  47883  prproropen  48111  stgrvtx  48573  stgriedg  48574  gpgvtx  48662  gpgiedg  48663