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

Syntax hints:   /\ wa 104   e. wcel 2209   {cab 2224   {crab 2532   C_ wss 3220

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 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 theorem 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 referenced by:  ssrab3  3334  ssrabeq  3336  ifssun  3652  rabexg  4274  pwnss  4291  undifexmid  4325  exmidexmid  4328  exmidsssnc  4335  onintrab2im  4660  ordtriexmidlem  4661  ontr2exmid  4667  ordtri2or2exmidlem  4668  onsucsssucexmid  4669  onsucelsucexmidlem  4671  tfis  4725  nnregexmid  4763  dmmptss  5279  ssimaex  5758  f1oresrab  5864  canth  6026  riotacl  6044  suppssdmg  6479  pmvalg  6923  ssfiexmid  7168  ssfiexmidt  7170  domfiexmid  7172  2omap  7308  ctssdccl  7441  ctssexmid  7480  genpelxp  7868  ltexprlempr  7965  cauappcvgprlemcl  8010  cauappcvgprlemladd  8015  caucvgprlemcl  8033  caucvgprprlemcl  8061  suplocexprlemex  8079  uzf  9903  supminfex  9976  rpre  10040  ixxf  10279  fzf  10394  infssuzex  10644  infssuzcldc  10646  zsupssdc  10651  expcl2lemap  10966  expclzaplem  10978  expge0  10990  expge1  10991  dvdsflip  12596  bitsf  12691  bitsfzolem  12699  gcddvds  12718  uzwodc  12792  nnwosdc  12794  nninfctlemfo  12795  lcmn0cl  12824  phicl2  12970  phimullem  12981  eulerthlemfi  12984  eulerthlemrprm  12985  eulerthlema  12986  eulerthlemh  12987  eulerthlemth  12988  phisum  12997  pcpremul  13050  ballotfilem2  13206  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemiex  13222  ballotfilem7  13257  ballotfilemth  13259  ennnfonelemg  13272  ennnfonelemh  13273  ctiunctlemuom  13305  issubmd  13758  mhmeql  13776  lspf  14698  mplbascoe  15005  mplbasss  15010  epttop  15114  neipsm  15178  cnpfval  15219  blfvalps  15409  blfps  15433  blf  15434  divcnap  15589  cdivcncfap  15628  cnopnap  15635  ivthinclemex  15666  limcdifap  15686  dvfgg  15712  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvcnp2cntop  15723  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731  dvrecap  15737  pellexlem3  16007  sgmval2  16012  sgmmul  16024  perfectlem2  16028  lgsfcl  16041  lgscl  16047  lgsquadlem1  16110  lgsquadlem2  16111  incistruhgr  16245  upgrss  16254  usgrss  16332  ushgredgedg  16381  ushgredgedgloop  16383  vtxdfifiun  16452  bdrabexg  16846  pw1map  16939  subctctexmid  16944