Theorem rabexd 5268

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  {crab 3391  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-in 3890  df-ss 3900  df-pw 4531

This theorem is referenced by:  rabex2  5269  zorn2lem1  10409  sylow2a  19585  psrascl  21953  evlslem6  22057  evlsvvval  22069  mhmcompl  22097  mhmcoaddmpl  22099  mhpaddcl  22139  mretopd  23075  cusgrexilem1  29526  vtxdgf  29558  mntoval  33061  tocycval  33189  fxpval  33246  prmidlval  33520  selvply1rhmlemb  33703  extvfvcl  33720  isprimroot  42578  primrootsunit1  42582  unitscyglem1  42680  evlsbagval  43036  mhpind  43044  stoweidlem35  46478  stoweidlem50  46493  stoweidlem57  46500  stoweidlem59  46502  subsaliuncllem  46800  subsaliuncl  46801  smflimlem1  47214  smflimlem2  47215  smflimlem3  47216  smflimlem6  47219  smfrec  47232  smfpimcclem  47250  smfsuplem1  47254  smfinflem  47260  smflimsuplem1  47263  smflimsuplem2  47264  smflimsuplem3  47265  smflimsuplem4  47266  smflimsuplem5  47267  smflimsuplem7  47269  fvmptrab  47755  prproropen  47983  stgrvtx  48445  stgriedg  48446  gpgvtx  48534  gpgiedg  48535