Theorem rabexg 4281

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  {crab 2532  Vcvv 2821   ⊆ wss 3220

This proof depends on 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 4251

This proof 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 used by:  rabex  4282  rabexd  4283  exmidsssnc  4342  exse  4483  frind  4499  elfvmptrab1  5804  elovmporab  6292  elovmporab1w  6293  suppval  6481  mpoxopoveq  6515  diffitest  7195  supex2g  7379  cc4f  7641  omctfn  13392  ismhm  13827  mhmex  13828  issubm  13838  issubg  14035  subgex  14038  isnsg  14064  isrim0  14577  issubrng  14616  issubrg  14638  rrgval  14679  lssex  14800  lsssetm  14802  psrval  15159  psrplusgg  15182  psraddcl  15184  epttop  15316  cldval  15325  neif  15367  neival  15369  cnfval  15420  cnovex  15422  cnpval  15424  hmeofn  15528  hmeofvalg  15529  ispsmet  15549  ismet  15570  isxmet  15571  blvalps  15614  blval  15615  cncfval  15798  clwwlkg  16839  clwwlknon  16875