Theorem rabexd 5304

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {crab 3412  Vcvv 3450

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 2147  ax-9 2155  ax-ext 2732  ax-sep 5251

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3906  df-ss 3916  df-pw 4559

This theorem is used by:  rabex2  5305  zorn2lem1  10499  sylow2a  19747  prmidlval  21526  psrascl  22194  evlslem6  22298  evlsvvval  22310  mhmcompl  22338  mhmcoaddmpl  22340  mhpaddcl  22380  mretopd  23318  plngval  29135  angmgmval  29274  cusgrexilem1  29900  vtxdgf  29932  mntoval  33423  tocycval  33549  fxpval  33606  selvply1rhmlemb  34030  extvfvcl  34047  isprimroot  42960  primrootsunit1  42964  unitscyglem1  43062  evlsbagval  43433  mhpind  43441  stoweidlem35  46864  stoweidlem50  46879  stoweidlem57  46886  stoweidlem59  46888  subsaliuncllem  47186  subsaliuncl  47187  smflimlem1  47600  smflimlem2  47601  smflimlem3  47602  smflimlem6  47605  smfrec  47618  smfpimcclem  47636  smfsuplem1  47640  smfinflem  47646  smflimsuplem1  47649  smflimsuplem2  47650  smflimsuplem3  47651  smflimsuplem4  47652  smflimsuplem5  47653  smflimsuplem7  47655  fvmptrab  48181  prproropen  48409  stgrvtx  48871  stgriedg  48872  gpgvtx  48960  gpgiedg  48961