Theorem rabexg 2798

Description: Separation Scheme in terms of a restricted class abstraction.

Assertion

Ref	Expression
rabexg	⊢ (A ∈ B → {x ∈ A∣φ} ∈ V)

Distinct variable group:   x,A

Proof of Theorem rabexg

Step	Hyp	Ref	Expression
1		ssrab2 2183	. 2 ⊢ {x ∈ A∣φ} ⊆ A
2		ssexg 2795	. 2 ⊢ (({x ∈ A∣φ} ⊆ A ⋀ A ∈ B) → {x ∈ A∣φ} ∈ V)
3	1, 2	mpan 699	1 ⊢ (A ∈ B → {x ∈ A∣φ} ∈ V)

Syntax hints:   → wi 3   ∈ wcel 994  {crab 1694  Vcvv 1857   ⊆ wss 2099

This theorem is referenced by:  rabex 2799  class2set 2808  abssexg 2825  scottex 4862  lbinfm 6216  ntrval 7886  blval 8047  blrn 8051  grpinvval 8284  grpinvf 8297  spwval2 8915  pjval 9515  fiv 10849  idrval 10904  fgsb 11082  fgsb2 11086  isfuna 11288  compsublem 11487  isfne3 11543  fnessref 11564  neibastop2lem3 11582  neibastop2lem4 11583  opnfbas 11629  fgf 11632  limfil 11675  indexa 11845  supex2g 11853

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-rab 1698  df-v 1858  df-in 2103  df-ss 2105

Copyright terms: Public domain