Theorem ssrab2 3310

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

Syntax hints:   /\ wa 104   e. wcel 2200   {cab 2215   {crab 2512   C_ wss 3198

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-in 3204  df-ss 3211

This theorem is referenced by:  ssrab3  3311  ssrabeq  3312  ifssun  3618  rabexg  4231  pwnss  4247  undifexmid  4281  exmidexmid  4284  exmidsssnc  4291  onintrab2im  4614  ordtriexmidlem  4615  ontr2exmid  4621  ordtri2or2exmidlem  4622  onsucsssucexmid  4623  onsucelsucexmidlem  4625  tfis  4679  nnregexmid  4717  dmmptss  5231  ssimaex  5703  f1oresrab  5808  canth  5964  riotacl  5982  pmvalg  6823  ssfiexmid  7058  domfiexmid  7060  ctssdccl  7301  ctssexmid  7340  genpelxp  7721  ltexprlempr  7818  cauappcvgprlemcl  7863  cauappcvgprlemladd  7868  caucvgprlemcl  7886  caucvgprprlemcl  7914  suplocexprlemex  7932  uzf  9748  supminfex  9821  rpre  9885  ixxf  10123  fzf  10237  infssuzex  10483  infssuzcldc  10485  zsupssdc  10488  expcl2lemap  10803  expclzaplem  10815  expge0  10827  expge1  10828  dvdsflip  12402  bitsf  12497  bitsfzolem  12505  gcddvds  12524  uzwodc  12598  nnwosdc  12600  nninfctlemfo  12601  lcmn0cl  12630  phicl2  12776  phimullem  12787  eulerthlemfi  12790  eulerthlemrprm  12791  eulerthlema  12792  eulerthlemh  12793  eulerthlemth  12794  phisum  12803  pcpremul  12856  ennnfonelemg  13014  ennnfonelemh  13015  ctiunctlemuom  13047  issubmd  13547  mhmeql  13565  lspf  14393  mplbascoe  14695  mplbasss  14700  epttop  14804  neipsm  14868  cnpfval  14909  blfvalps  15099  blfps  15123  blf  15124  divcnap  15279  cdivcncfap  15318  cnopnap  15325  ivthinclemex  15356  limcdifap  15376  dvfgg  15402  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvcnp2cntop  15413  dvaddxxbr  15415  dvmulxxbr  15416  dvcoapbr  15421  dvrecap  15427  sgmval2  15698  sgmmul  15710  perfectlem2  15714  lgsfcl  15727  lgscl  15733  lgsquadlem1  15796  lgsquadlem2  15797  incistruhgr  15931  upgrss  15940  usgrss  16016  ushgredgedg  16065  ushgredgedgloop  16067  vtxdfifiun  16103  bdrabexg  16437  2omap  16530  pw1map  16532  subctctexmid  16537