Theorem ssrab2 3286

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

Syntax hints:   /\ wa 104   e. wcel 2178   {cab 2193   {crab 2490   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rab 2495  df-in 3180  df-ss 3187

This theorem is referenced by:  ssrab3  3287  ssrabeq  3288  ifssun  3594  rabexg  4203  pwnss  4219  undifexmid  4253  exmidexmid  4256  exmidsssnc  4263  onintrab2im  4584  ordtriexmidlem  4585  ontr2exmid  4591  ordtri2or2exmidlem  4592  onsucsssucexmid  4593  onsucelsucexmidlem  4595  tfis  4649  nnregexmid  4687  dmmptss  5198  ssimaex  5663  f1oresrab  5768  canth  5920  riotacl  5937  pmvalg  6769  ssfiexmid  6999  domfiexmid  7001  ctssdccl  7239  ctssexmid  7278  genpelxp  7659  ltexprlempr  7756  cauappcvgprlemcl  7801  cauappcvgprlemladd  7806  caucvgprlemcl  7824  caucvgprprlemcl  7852  suplocexprlemex  7870  uzf  9686  supminfex  9753  rpre  9817  ixxf  10055  fzf  10169  infssuzex  10413  infssuzcldc  10415  zsupssdc  10418  expcl2lemap  10733  expclzaplem  10745  expge0  10757  expge1  10758  dvdsflip  12277  bitsf  12372  bitsfzolem  12380  gcddvds  12399  uzwodc  12473  nnwosdc  12475  nninfctlemfo  12476  lcmn0cl  12505  phicl2  12651  phimullem  12662  eulerthlemfi  12665  eulerthlemrprm  12666  eulerthlema  12667  eulerthlemh  12668  eulerthlemth  12669  phisum  12678  pcpremul  12731  ennnfonelemg  12889  ennnfonelemh  12890  ctiunctlemuom  12922  issubmd  13421  mhmeql  13439  lspf  14266  mplbascoe  14568  mplbasss  14573  epttop  14677  neipsm  14741  cnpfval  14782  blfvalps  14972  blfps  14996  blf  14997  divcnap  15152  cdivcncfap  15191  cnopnap  15198  ivthinclemex  15229  limcdifap  15249  dvfgg  15275  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvcnp2cntop  15286  dvaddxxbr  15288  dvmulxxbr  15289  dvcoapbr  15294  dvrecap  15300  sgmval2  15571  sgmmul  15583  perfectlem2  15587  lgsfcl  15600  lgscl  15606  lgsquadlem1  15669  lgsquadlem2  15670  incistruhgr  15801  upgrss  15810  bdrabexg  16041  2omap  16132  pw1map  16134  subctctexmid  16139