Theorem ssrab2 3333

Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.)

Assertion

Ref	Expression
ssrab2	|- { x e. A | ph } C_ A

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem ssrab2

Step	Hyp	Ref	Expression
1		df-rab 2537	. 2 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
2		ssab2 3332	. 2 |- { x | ( x e. A /\ ph ) } C_ A
3	1, 2	eqsstri 3280	1 |- { x e. A | ph } C_ A

This proof depends on syntax axioms:   /\ wa 104   e. wcel 2209   {cab 2224   {crab 2532   C_ 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

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

This theorem is used by:  ssrab3  3334  ssrabeq  3336  ifssun  3655  rabexg  4279  pwnss  4296  undifexmid  4330  exmidexmid  4333  exmidsssnc  4340  onintrab2im  4665  ordtriexmidlem  4666  ontr2exmid  4672  ordtri2or2exmidlem  4673  onsucsssucexmid  4674  onsucelsucexmidlem  4676  tfis  4730  nnregexmid  4768  dmmptss  5284  ssimaex  5764  f1oresrab  5873  canth  6036  riotacl  6054  suppssdmg  6489  pmvalg  6933  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  2omap  7318  ctssdccl  7451  ctssexmid  7490  genpelxp  7878  ltexprlempr  7975  cauappcvgprlemcl  8020  cauappcvgprlemladd  8025  caucvgprlemcl  8043  caucvgprprlemcl  8071  suplocexprlemex  8089  uzf  9933  supminfex  10006  rpre  10071  ixxf  10310  fzf  10425  infssuzex  10676  infssuzcldc  10678  zsupssdc  10683  expcl2lemap  11001  expclzaplem  11013  expge0  11025  expge1  11026  dvdsflip  12634  bitsf  12729  bitsfzolem  12737  gcddvds  12756  uzwodc  12830  nnwosdc  12832  nninfctlemfo  12833  lcmn0cl  12862  phicl2  13012  phimullem  13023  eulerthlemfi  13026  eulerthlemrprm  13027  eulerthlema  13028  eulerthlemh  13029  eulerthlemth  13030  phisum  13039  pcpremul  13092  ballotfilem2  13277  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemiex  13293  ballotfilem7  13328  ballotfilemth  13330  ennnfonelemg  13343  ennnfonelemh  13344  ctiunctlemuom  13376  issubmd  13830  mhmeql  13848  lspf  14775  asplss  15065  aspsubrg  15067  mplbascoe  15131  mplbasss  15136  epttop  15240  neipsm  15304  cnpfval  15345  blfvalps  15535  blfps  15559  blf  15560  divcnap  15715  cdivcncfap  15754  cnopnap  15761  ivthinclemex  15792  limcdifap  15812  dvfgg  15838  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvcnp2cntop  15849  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvrecap  15863  pellexlem3  16150  sgmval2  16165  sgmmul  16191  ppiqub  16194  perfectlem2  16198  lgsfcl  16225  lgscl  16231  lgsquadlem1  16294  lgsquadlem2  16295  incistruhgr  16429  upgrss  16438  usgrss  16516  ushgredgedg  16565  ushgredgedgloop  16567  vtxdfifiun  16636  bdrabexg  17030  pw1map  17123  subctctexmid  17128  stnot  17137  wexmiddc  17140