Theorem ssrab2 3312

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

Syntax hints:   /\ wa 104   e. wcel 2202   {cab 2217   {crab 2514   C_ wss 3200

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-in 3206  df-ss 3213

This theorem is referenced by:  ssrab3  3313  ssrabeq  3314  ifssun  3620  rabexg  4233  pwnss  4249  undifexmid  4283  exmidexmid  4286  exmidsssnc  4293  onintrab2im  4616  ordtriexmidlem  4617  ontr2exmid  4623  ordtri2or2exmidlem  4624  onsucsssucexmid  4625  onsucelsucexmidlem  4627  tfis  4681  nnregexmid  4719  dmmptss  5233  ssimaex  5707  f1oresrab  5812  canth  5968  riotacl  5986  pmvalg  6827  ssfiexmid  7062  ssfiexmidt  7064  domfiexmid  7066  ctssdccl  7309  ctssexmid  7348  genpelxp  7730  ltexprlempr  7827  cauappcvgprlemcl  7872  cauappcvgprlemladd  7877  caucvgprlemcl  7895  caucvgprprlemcl  7923  suplocexprlemex  7941  uzf  9757  supminfex  9830  rpre  9894  ixxf  10132  fzf  10246  infssuzex  10492  infssuzcldc  10494  zsupssdc  10497  expcl2lemap  10812  expclzaplem  10824  expge0  10836  expge1  10837  dvdsflip  12411  bitsf  12506  bitsfzolem  12514  gcddvds  12533  uzwodc  12607  nnwosdc  12609  nninfctlemfo  12610  lcmn0cl  12639  phicl2  12785  phimullem  12796  eulerthlemfi  12799  eulerthlemrprm  12800  eulerthlema  12801  eulerthlemh  12802  eulerthlemth  12803  phisum  12812  pcpremul  12865  ennnfonelemg  13023  ennnfonelemh  13024  ctiunctlemuom  13056  issubmd  13556  mhmeql  13574  lspf  14402  mplbascoe  14704  mplbasss  14709  epttop  14813  neipsm  14877  cnpfval  14918  blfvalps  15108  blfps  15132  blf  15133  divcnap  15288  cdivcncfap  15327  cnopnap  15334  ivthinclemex  15365  limcdifap  15385  dvfgg  15411  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvcnp2cntop  15422  dvaddxxbr  15424  dvmulxxbr  15425  dvcoapbr  15430  dvrecap  15436  sgmval2  15707  sgmmul  15719  perfectlem2  15723  lgsfcl  15736  lgscl  15742  lgsquadlem1  15805  lgsquadlem2  15806  incistruhgr  15940  upgrss  15949  usgrss  16027  ushgredgedg  16076  ushgredgedgloop  16078  vtxdfifiun  16147  bdrabexg  16501  2omap  16594  pw1map  16596  subctctexmid  16601