Theorem rabexd 5295

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {crab 3405  Vcvv 3447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931  df-pw 4565

This theorem is referenced by:  rabex2  5296  zorn2lem1  10449  sylow2a  19549  psrascl  21888  evlslem6  21988  mhpaddcl  22038  mhmcompl  22267  mhmcoaddmpl  22268  mretopd  22979  cusgrexilem1  29366  vtxdgf  29399  mntoval  32908  tocycval  33065  fxpval  33122  prmidlval  33408  isprimroot  42081  primrootsunit1  42085  unitscyglem1  42183  evlsvvval  42551  evlsbagval  42554  mhpind  42582  stoweidlem35  46033  stoweidlem50  46048  stoweidlem57  46055  stoweidlem59  46057  subsaliuncllem  46355  subsaliuncl  46356  smflimlem1  46769  smflimlem2  46770  smflimlem3  46771  smflimlem6  46774  smfrec  46787  smfpimcclem  46805  smfsuplem1  46809  smfinflem  46815  smflimsuplem1  46818  smflimsuplem2  46819  smflimsuplem3  46820  smflimsuplem4  46821  smflimsuplem5  46822  smflimsuplem7  46824  fvmptrab  47293  prproropen  47509  stgrvtx  47953  stgriedg  47954  gpgvtx  48034  gpgiedg  48035