Theorem ssrab2 3238

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

Syntax hints:   /\ wa 104   e. wcel 2146   {cab 2161   {crab 2457   C_ wss 3127

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rab 2462  df-in 3133  df-ss 3140

This theorem is referenced by:  ssrab3  3239  ssrabeq  3240  ifssun  3546  rabexg  4141  pwnss  4154  undifexmid  4188  exmidexmid  4191  exmidsssnc  4198  onintrab2im  4511  ordtriexmidlem  4512  ontr2exmid  4518  ordtri2or2exmidlem  4519  onsucsssucexmid  4520  onsucelsucexmidlem  4522  tfis  4576  nnregexmid  4614  dmmptss  5117  ssimaex  5569  f1oresrab  5673  canth  5819  riotacl  5835  pmvalg  6649  ssfiexmid  6866  domfiexmid  6868  ctssdccl  7100  ctssexmid  7138  genpelxp  7485  ltexprlempr  7582  cauappcvgprlemcl  7627  cauappcvgprlemladd  7632  caucvgprlemcl  7650  caucvgprprlemcl  7678  suplocexprlemex  7696  uzf  9502  supminfex  9568  rpre  9629  ixxf  9867  fzf  9981  expcl2lemap  10500  expclzaplem  10512  expge0  10524  expge1  10525  dvdsflip  11822  infssuzex  11915  infssuzcldc  11917  zsupssdc  11920  gcddvds  11929  uzwodc  12003  nnwosdc  12005  lcmn0cl  12033  phicl2  12179  phimullem  12190  eulerthlemfi  12193  eulerthlemrprm  12194  eulerthlema  12195  eulerthlemh  12196  eulerthlemth  12197  phisum  12205  pcpremul  12258  ennnfonelemg  12369  ennnfonelemh  12370  ctiunctlemuom  12402  issubmd  12725  mhmeql  12736  epttop  13141  neipsm  13205  cnpfval  13246  blfvalps  13436  blfps  13460  blf  13461  divcnap  13606  cdivcncfap  13638  cnopnap  13645  ivthinclemex  13671  limcdifap  13682  dvfgg  13708  dvidlemap  13711  dvcnp2cntop  13714  dvaddxxbr  13716  dvmulxxbr  13717  dvcoapbr  13722  dvrecap  13728  lgsfcl  13960  lgscl  13966  bdrabexg  14198  subctctexmid  14291