Theorem ssrab2 3265

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

Syntax hints:   /\ wa 104   e. wcel 2164   {cab 2179   {crab 2476   C_ wss 3154

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rab 2481  df-in 3160  df-ss 3167

This theorem is referenced by:  ssrab3  3266  ssrabeq  3267  ifssun  3572  rabexg  4173  pwnss  4189  undifexmid  4223  exmidexmid  4226  exmidsssnc  4233  onintrab2im  4551  ordtriexmidlem  4552  ontr2exmid  4558  ordtri2or2exmidlem  4559  onsucsssucexmid  4560  onsucelsucexmidlem  4562  tfis  4616  nnregexmid  4654  dmmptss  5163  ssimaex  5619  f1oresrab  5724  canth  5872  riotacl  5889  pmvalg  6715  ssfiexmid  6934  domfiexmid  6936  ctssdccl  7172  ctssexmid  7211  genpelxp  7573  ltexprlempr  7670  cauappcvgprlemcl  7715  cauappcvgprlemladd  7720  caucvgprlemcl  7738  caucvgprprlemcl  7766  suplocexprlemex  7784  uzf  9598  supminfex  9665  rpre  9729  ixxf  9967  fzf  10081  expcl2lemap  10625  expclzaplem  10637  expge0  10649  expge1  10650  dvdsflip  11996  infssuzex  12089  infssuzcldc  12091  zsupssdc  12094  gcddvds  12103  uzwodc  12177  nnwosdc  12179  nninfctlemfo  12180  lcmn0cl  12209  phicl2  12355  phimullem  12366  eulerthlemfi  12369  eulerthlemrprm  12370  eulerthlema  12371  eulerthlemh  12372  eulerthlemth  12373  phisum  12381  pcpremul  12434  ennnfonelemg  12563  ennnfonelemh  12564  ctiunctlemuom  12596  issubmd  13049  mhmeql  13067  lspf  13888  epttop  14269  neipsm  14333  cnpfval  14374  blfvalps  14564  blfps  14588  blf  14589  divcnap  14744  cdivcncfap  14783  cnopnap  14790  ivthinclemex  14821  limcdifap  14841  dvfgg  14867  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvcnp2cntop  14878  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  dvrecap  14892  lgsfcl  15165  lgscl  15171  lgsquadlem1  15234  lgsquadlem2  15235  bdrabexg  15468  subctctexmid  15561