Theorem rabexd 5312

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  {crab 3418  Vcvv 3457

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-in 3913  df-ss 3923  df-pw 4566

This theorem is used by:  rabex2  5313  zorn2lem1  10495  sylow2a  19733  prmidlval  21512  psrascl  22178  evlslem6  22282  evlsvvval  22294  mhmcompl  22322  mhmcoaddmpl  22324  mhpaddcl  22364  mretopd  23299  plngval  29110  cusgrexilem1  29847  vtxdgf  29879  mntoval  33366  tocycval  33492  fxpval  33549  selvply1rhmlemb  33973  extvfvcl  33990  isprimroot  42918  primrootsunit1  42922  unitscyglem1  43020  evlsbagval  43376  mhpind  43384  stoweidlem35  46807  stoweidlem50  46822  stoweidlem57  46829  stoweidlem59  46831  subsaliuncllem  47129  subsaliuncl  47130  smflimlem1  47543  smflimlem2  47544  smflimlem3  47545  smflimlem6  47548  smfrec  47561  smfpimcclem  47579  smfsuplem1  47583  smfinflem  47589  smflimsuplem1  47592  smflimsuplem2  47593  smflimsuplem3  47594  smflimsuplem4  47595  smflimsuplem5  47596  smflimsuplem7  47598  fvmptrab  48087  prproropen  48315  stgrvtx  48777  stgriedg  48778  gpgvtx  48866  gpgiedg  48867