Theorem rabexd 5283

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {crab 3397  Vcvv 3438

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 2115  ax-9 2123  ax-ext 2706  ax-sep 5239

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 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-in 3906  df-ss 3916  df-pw 4554

This theorem is referenced by:  rabex2  5284  zorn2lem1  10404  sylow2a  19546  psrascl  21932  evlslem6  22034  evlsvvval  22046  mhpaddcl  22092  mhmcompl  22322  mhmcoaddmpl  22323  mretopd  23034  cusgrexilem1  29461  vtxdgf  29494  mntoval  33013  tocycval  33139  fxpval  33196  prmidlval  33467  extvfvcl  33650  isprimroot  42286  primrootsunit1  42290  unitscyglem1  42388  evlsbagval  42754  mhpind  42779  stoweidlem35  46221  stoweidlem50  46236  stoweidlem57  46243  stoweidlem59  46245  subsaliuncllem  46543  subsaliuncl  46544  smflimlem1  46957  smflimlem2  46958  smflimlem3  46959  smflimlem6  46962  smfrec  46975  smfpimcclem  46993  smfsuplem1  46997  smfinflem  47003  smflimsuplem1  47006  smflimsuplem2  47007  smflimsuplem3  47008  smflimsuplem4  47009  smflimsuplem5  47010  smflimsuplem7  47012  fvmptrab  47480  prproropen  47696  stgrvtx  48142  stgriedg  48143  gpgvtx  48231  gpgiedg  48232