Theorem rabexd 5310

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  {crab 3416  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3912  df-ss 3922  df-pw 4564

This theorem is referenced by:  rabex2  5311  zorn2lem1  10475  sylow2a  19684  prmidlval  21462  psrascl  22128  evlslem6  22232  evlsvvval  22244  mhmcompl  22272  mhmcoaddmpl  22274  mhpaddcl  22314  mretopd  23249  plngval  29059  cusgrexilem1  29789  vtxdgf  29821  mntoval  33302  tocycval  33428  fxpval  33485  selvply1rhmlemb  33909  extvfvcl  33926  isprimroot  42860  primrootsunit1  42864  unitscyglem1  42962  evlsbagval  43318  mhpind  43326  stoweidlem35  46749  stoweidlem50  46764  stoweidlem57  46771  stoweidlem59  46773  subsaliuncllem  47071  subsaliuncl  47072  smflimlem1  47485  smflimlem2  47486  smflimlem3  47487  smflimlem6  47490  smfrec  47503  smfpimcclem  47521  smfsuplem1  47525  smfinflem  47531  smflimsuplem1  47534  smflimsuplem2  47535  smflimsuplem3  47536  smflimsuplem4  47537  smflimsuplem5  47538  smflimsuplem7  47540  fvmptrab  48029  prproropen  48257  stgrvtx  48719  stgriedg  48720  gpgvtx  48808  gpgiedg  48809