Theorem rabexd 5311

Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5312. (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 2873	1 ⊢ (𝜑 → 𝐵 ∈ V)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  {crab 3423  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-in 3920  df-ss 3930  df-pw 4569

This theorem is referenced by:  rabex2  5312  zorn2lem1  10479  sylow2a  19688  prmidlval  21432  psrascl  22096  evlslem6  22200  evlsvvval  22212  mhmcompl  22240  mhmcoaddmpl  22242  mhpaddcl  22282  mretopd  23217  plngval  29016  cusgrexilem1  29729  vtxdgf  29761  mntoval  33242  tocycval  33368  fxpval  33425  selvply1rhmlemb  33853  extvfvcl  33870  isprimroot  42749  primrootsunit1  42753  unitscyglem1  42851  evlsbagval  43209  mhpind  43217  stoweidlem35  46640  stoweidlem50  46655  stoweidlem57  46662  stoweidlem59  46664  subsaliuncllem  46962  subsaliuncl  46963  smflimlem1  47376  smflimlem2  47377  smflimlem3  47378  smflimlem6  47381  smfrec  47394  smfpimcclem  47412  smfsuplem1  47416  smfinflem  47422  smflimsuplem1  47425  smflimsuplem2  47426  smflimsuplem3  47427  smflimsuplem4  47428  smflimsuplem5  47429  smflimsuplem7  47431  fvmptrab  47917  prproropen  48145  stgrvtx  48607  stgriedg  48608  gpgvtx  48696  gpgiedg  48697