Theorem ssrab2 3278

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 2493	. 2 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
2		ssab2 3277	. 2 |- { x | ( x e. A /\ ph ) } C_ A
3	1, 2	eqsstri 3225	1 |- { x e. A | ph } C_ A

Syntax hints:   /\ wa 104   e. wcel 2176   {cab 2191   {crab 2488   C_ wss 3166

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rab 2493  df-in 3172  df-ss 3179

This theorem is referenced by:  ssrab3  3279  ssrabeq  3280  ifssun  3585  rabexg  4187  pwnss  4203  undifexmid  4237  exmidexmid  4240  exmidsssnc  4247  onintrab2im  4566  ordtriexmidlem  4567  ontr2exmid  4573  ordtri2or2exmidlem  4574  onsucsssucexmid  4575  onsucelsucexmidlem  4577  tfis  4631  nnregexmid  4669  dmmptss  5179  ssimaex  5640  f1oresrab  5745  canth  5897  riotacl  5914  pmvalg  6746  ssfiexmid  6973  domfiexmid  6975  ctssdccl  7213  ctssexmid  7252  genpelxp  7624  ltexprlempr  7721  cauappcvgprlemcl  7766  cauappcvgprlemladd  7771  caucvgprlemcl  7789  caucvgprprlemcl  7817  suplocexprlemex  7835  uzf  9651  supminfex  9718  rpre  9782  ixxf  10020  fzf  10134  infssuzex  10376  infssuzcldc  10378  zsupssdc  10381  expcl2lemap  10696  expclzaplem  10708  expge0  10720  expge1  10721  dvdsflip  12162  bitsf  12257  bitsfzolem  12265  gcddvds  12284  uzwodc  12358  nnwosdc  12360  nninfctlemfo  12361  lcmn0cl  12390  phicl2  12536  phimullem  12547  eulerthlemfi  12550  eulerthlemrprm  12551  eulerthlema  12552  eulerthlemh  12553  eulerthlemth  12554  phisum  12563  pcpremul  12616  ennnfonelemg  12774  ennnfonelemh  12775  ctiunctlemuom  12807  issubmd  13306  mhmeql  13324  lspf  14151  mplbascoe  14453  mplbasss  14458  epttop  14562  neipsm  14626  cnpfval  14667  blfvalps  14857  blfps  14881  blf  14882  divcnap  15037  cdivcncfap  15076  cnopnap  15083  ivthinclemex  15114  limcdifap  15134  dvfgg  15160  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvcnp2cntop  15171  dvaddxxbr  15173  dvmulxxbr  15174  dvcoapbr  15179  dvrecap  15185  sgmval2  15456  sgmmul  15468  perfectlem2  15472  lgsfcl  15485  lgscl  15491  lgsquadlem1  15554  lgsquadlem2  15555  bdrabexg  15842  2omap  15932  subctctexmid  15937