Theorem rabexg 4274

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 3333	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
2		ssexg 4267	. 2 ⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
3	1, 2	mpan 428	1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2209  {crab 2532  Vcvv 2821   ⊆ wss 3220

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4244

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-v 2823  df-in 3226  df-ss 3233

This theorem is referenced by:  rabex  4275  rabexd  4276  exmidsssnc  4335  exse  4476  frind  4492  elfvmptrab1  5794  elovmporab  6279  elovmporab1w  6280  suppval  6467  mpoxopoveq  6501  diffitest  7181  supex2g  7363  cc4f  7625  omctfn  13312  ismhm  13745  mhmex  13746  issubm  13756  issubg  13953  subgex  13956  isnsg  13982  isrim0  14441  issubrng  14480  issubrg  14502  rrgval  14543  lssex  14663  lsssetm  14665  psrval  14973  psrplusgg  14992  psraddcl  14994  epttop  15114  cldval  15123  neif  15165  neival  15167  cnfval  15218  cnovex  15220  cnpval  15222  hmeofn  15326  hmeofvalg  15327  ispsmet  15347  ismet  15368  isxmet  15369  blvalps  15412  blval  15413  cncfval  15596  clwwlkg  16548  clwwlknon  16584