Theorem ssrab2 3269

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

Syntax hints:   /\ wa 104   e. wcel 2167   {cab 2182   {crab 2479   C_ wss 3157

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rab 2484  df-in 3163  df-ss 3170

This theorem is referenced by:  ssrab3  3270  ssrabeq  3271  ifssun  3576  rabexg  4177  pwnss  4193  undifexmid  4227  exmidexmid  4230  exmidsssnc  4237  onintrab2im  4555  ordtriexmidlem  4556  ontr2exmid  4562  ordtri2or2exmidlem  4563  onsucsssucexmid  4564  onsucelsucexmidlem  4566  tfis  4620  nnregexmid  4658  dmmptss  5167  ssimaex  5625  f1oresrab  5730  canth  5878  riotacl  5895  pmvalg  6727  ssfiexmid  6946  domfiexmid  6948  ctssdccl  7186  ctssexmid  7225  genpelxp  7595  ltexprlempr  7692  cauappcvgprlemcl  7737  cauappcvgprlemladd  7742  caucvgprlemcl  7760  caucvgprprlemcl  7788  suplocexprlemex  7806  uzf  9621  supminfex  9688  rpre  9752  ixxf  9990  fzf  10104  infssuzex  10340  infssuzcldc  10342  zsupssdc  10345  expcl2lemap  10660  expclzaplem  10672  expge0  10684  expge1  10685  dvdsflip  12033  bitsf  12128  bitsfzolem  12136  gcddvds  12155  uzwodc  12229  nnwosdc  12231  nninfctlemfo  12232  lcmn0cl  12261  phicl2  12407  phimullem  12418  eulerthlemfi  12421  eulerthlemrprm  12422  eulerthlema  12423  eulerthlemh  12424  eulerthlemth  12425  phisum  12434  pcpremul  12487  ennnfonelemg  12645  ennnfonelemh  12646  ctiunctlemuom  12678  issubmd  13176  mhmeql  13194  lspf  14021  epttop  14410  neipsm  14474  cnpfval  14515  blfvalps  14705  blfps  14729  blf  14730  divcnap  14885  cdivcncfap  14924  cnopnap  14931  ivthinclemex  14962  limcdifap  14982  dvfgg  15008  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvcnp2cntop  15019  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  dvrecap  15033  sgmval2  15304  sgmmul  15316  perfectlem2  15320  lgsfcl  15333  lgscl  15339  lgsquadlem1  15402  lgsquadlem2  15403  bdrabexg  15636  2omap  15726  subctctexmid  15731