Theorem rabexg 4176

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.)

Assertion

Ref	Expression
rabexg	⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem rabexg

Step	Hyp	Ref	Expression
1		ssrab2 3268	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
2		ssexg 4172	. 2 ⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
3	1, 2	mpan 424	1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2167  {crab 2479  Vcvv 2763   ⊆ wss 3157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4151

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rab 2484  df-v 2765  df-in 3163  df-ss 3170

This theorem is referenced by:  rabex  4177  rabexd  4178  exmidsssnc  4236  exse  4371  frind  4387  elfvmptrab1  5656  elovmporab  6123  elovmporab1w  6124  mpoxopoveq  6298  diffitest  6948  supex2g  7099  cc4f  7336  omctfn  12660  ismhm  13093  mhmex  13094  issubm  13104  issubg  13303  subgex  13306  isnsg  13332  isrim0  13717  issubrng  13755  issubrg  13777  rrgval  13818  lssex  13910  lsssetm  13912  psrval  14220  psrplusgg  14230  psraddcl  14232  epttop  14326  cldval  14335  neif  14377  neival  14379  cnfval  14430  cnovex  14432  cnpval  14434  hmeofn  14538  hmeofvalg  14539  ispsmet  14559  ismet  14580  isxmet  14581  blvalps  14624  blval  14625  cncfval  14808