Theorem rabexg 4195

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

Syntax hints:   → wi 4   ∈ wcel 2177  {crab 2489  Vcvv 2773   ⊆ wss 3170

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-sep 4170

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rab 2494  df-v 2775  df-in 3176  df-ss 3183

This theorem is referenced by:  rabex  4196  rabexd  4197  exmidsssnc  4255  exse  4391  frind  4407  elfvmptrab1  5687  elovmporab  6159  elovmporab1w  6160  mpoxopoveq  6339  diffitest  6999  supex2g  7150  cc4f  7401  omctfn  12889  ismhm  13368  mhmex  13369  issubm  13379  issubg  13584  subgex  13587  isnsg  13613  isrim0  13998  issubrng  14036  issubrg  14058  rrgval  14099  lssex  14191  lsssetm  14193  psrval  14503  psrplusgg  14515  psraddcl  14517  epttop  14637  cldval  14646  neif  14688  neival  14690  cnfval  14741  cnovex  14743  cnpval  14745  hmeofn  14849  hmeofvalg  14850  ispsmet  14870  ismet  14891  isxmet  14892  blvalps  14935  blval  14936  cncfval  15119