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  9924  supminfex  9997  rpre  10061  ixxf  10300  fzf  10415  infssuzex  10666  infssuzcldc  10668  zsupssdc  10673  expcl2lemap  10988  expclzaplem  11000  expge0  11012  expge1  11013  dvdsflip  12618  bitsf  12713  bitsfzolem  12721  gcddvds  12740  uzwodc  12814  nnwosdc  12816  nninfctlemfo  12817  lcmn0cl  12846  phicl2  12992  phimullem  13003  eulerthlemfi  13006  eulerthlemrprm  13007  eulerthlema  13008  eulerthlemh  13009  eulerthlemth  13010  phisum  13019  pcpremul  13072  ballotfilem2  13228  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemiex  13244  ballotfilem7  13279  ballotfilemth  13281  ennnfonelemg  13294  ennnfonelemh  13295  ctiunctlemuom  13327  issubmd  13781  mhmeql  13799  lspf  14726  asplss  15016  aspsubrg  15018  mplbascoe  15082  mplbasss  15087  epttop  15191  neipsm  15255  cnpfval  15296  blfvalps  15486  blfps  15510  blf  15511  divcnap  15666  cdivcncfap  15705  cnopnap  15712  ivthinclemex  15743  limcdifap  15763  dvfgg  15789  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvcnp2cntop  15800  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808  dvrecap  15814  pellexlem3  16093  sgmval2  16098  sgmmul  16110  perfectlem2  16114  lgsfcl  16127  lgscl  16133  lgsquadlem1  16196  lgsquadlem2  16197  incistruhgr  16331  upgrss  16340  usgrss  16418  ushgredgedg  16467  ushgredgedgloop  16469  vtxdfifiun  16538  bdrabexg  16932  pw1map  17025  subctctexmid  17030  stnot  17039  wexmiddc  17042