Theorem ssrab2 3222

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

Syntax hints:   /\ wa 103   e. wcel 2135   {cab 2150   {crab 2446   C_ wss 3111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-rab 2451  df-in 3117  df-ss 3124

This theorem is referenced by:  ssrab3  3223  ssrabeq  3224  ifssun  3529  rabexg  4119  pwnss  4132  undifexmid  4166  exmidexmid  4169  exmidsssnc  4176  onintrab2im  4489  ordtriexmidlem  4490  ontr2exmid  4496  ordtri2or2exmidlem  4497  onsucsssucexmid  4498  onsucelsucexmidlem  4500  tfis  4554  nnregexmid  4592  dmmptss  5094  ssimaex  5541  f1oresrab  5644  canth  5790  riotacl  5806  pmvalg  6616  ssfiexmid  6833  domfiexmid  6835  ctssdccl  7067  ctssexmid  7105  genpelxp  7443  ltexprlempr  7540  cauappcvgprlemcl  7585  cauappcvgprlemladd  7590  caucvgprlemcl  7608  caucvgprprlemcl  7636  suplocexprlemex  7654  uzf  9460  supminfex  9526  rpre  9587  ixxf  9825  fzf  9939  expcl2lemap  10457  expclzaplem  10469  expge0  10481  expge1  10482  dvdsflip  11774  infssuzex  11867  infssuzcldc  11869  zsupssdc  11872  gcddvds  11881  lcmn0cl  11979  phicl2  12123  phimullem  12134  eulerthlemfi  12137  eulerthlemrprm  12138  eulerthlema  12139  eulerthlemh  12140  eulerthlemth  12141  phisum  12149  pcpremul  12202  ennnfonelemg  12273  ennnfonelemh  12274  ctiunctlemuom  12306  epttop  12631  neipsm  12695  cnpfval  12736  blfvalps  12926  blfps  12950  blf  12951  divcnap  13096  cdivcncfap  13128  cnopnap  13135  ivthinclemex  13161  limcdifap  13172  dvfgg  13198  dvidlemap  13201  dvcnp2cntop  13204  dvaddxxbr  13206  dvmulxxbr  13207  dvcoapbr  13212  dvrecap  13218  bdrabexg  13623  subctctexmid  13715