Theorem rabexd 5276

Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5277. (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 5273	. . 3 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V)
4	2, 3	syl 17	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V)
5	1, 4	eqeltrid 2835	1 ⊢ (𝜑 → 𝐵 ∈ V)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  {crab 3395  Vcvv 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914  df-pw 4549

This theorem is referenced by:  rabex2  5277  zorn2lem1  10387  sylow2a  19531  psrascl  21916  evlslem6  22016  mhpaddcl  22066  mhmcompl  22295  mhmcoaddmpl  22296  mretopd  23007  cusgrexilem1  29417  vtxdgf  29450  mntoval  32963  tocycval  33077  fxpval  33134  prmidlval  33402  isprimroot  42134  primrootsunit1  42138  unitscyglem1  42236  evlsvvval  42604  evlsbagval  42607  mhpind  42635  stoweidlem35  46081  stoweidlem50  46096  stoweidlem57  46103  stoweidlem59  46105  subsaliuncllem  46403  subsaliuncl  46404  smflimlem1  46817  smflimlem2  46818  smflimlem3  46819  smflimlem6  46822  smfrec  46835  smfpimcclem  46853  smfsuplem1  46857  smfinflem  46863  smflimsuplem1  46866  smflimsuplem2  46867  smflimsuplem3  46868  smflimsuplem4  46869  smflimsuplem5  46870  smflimsuplem7  46872  fvmptrab  47331  prproropen  47547  stgrvtx  47993  stgriedg  47994  gpgvtx  48082  gpgiedg  48083