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  5969  riotacl  5987  pmvalg  6828  ssfiexmid  7063  ssfiexmidt  7065  domfiexmid  7067  ctssdccl  7310  ctssexmid  7349  genpelxp  7731  ltexprlempr  7828  cauappcvgprlemcl  7873  cauappcvgprlemladd  7878  caucvgprlemcl  7896  caucvgprprlemcl  7924  suplocexprlemex  7942  uzf  9758  supminfex  9831  rpre  9895  ixxf  10133  fzf  10247  infssuzex  10494  infssuzcldc  10496  zsupssdc  10499  expcl2lemap  10814  expclzaplem  10826  expge0  10838  expge1  10839  dvdsflip  12430  bitsf  12525  bitsfzolem  12533  gcddvds  12552  uzwodc  12626  nnwosdc  12628  nninfctlemfo  12629  lcmn0cl  12658  phicl2  12804  phimullem  12815  eulerthlemfi  12818  eulerthlemrprm  12819  eulerthlema  12820  eulerthlemh  12821  eulerthlemth  12822  phisum  12831  pcpremul  12884  ennnfonelemg  13042  ennnfonelemh  13043  ctiunctlemuom  13075  issubmd  13575  mhmeql  13593  lspf  14422  mplbascoe  14724  mplbasss  14729  epttop  14833  neipsm  14897  cnpfval  14938  blfvalps  15128  blfps  15152  blf  15153  divcnap  15308  cdivcncfap  15347  cnopnap  15354  ivthinclemex  15385  limcdifap  15405  dvfgg  15431  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvcnp2cntop  15442  dvaddxxbr  15444  dvmulxxbr  15445  dvcoapbr  15450  dvrecap  15456  sgmval2  15727  sgmmul  15739  perfectlem2  15743  lgsfcl  15756  lgscl  15762  lgsquadlem1  15825  lgsquadlem2  15826  incistruhgr  15960  upgrss  15969  usgrss  16047  ushgredgedg  16096  ushgredgedgloop  16098  vtxdfifiun  16167  bdrabexg  16552  2omap  16645  pw1map  16647  subctctexmid  16652