Theorem ssrab2 3227

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

Syntax hints:   /\ wa 103   e. wcel 2136   {cab 2151   {crab 2448   C_ wss 3116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-rab 2453  df-in 3122  df-ss 3129

This theorem is referenced by:  ssrab3  3228  ssrabeq  3229  ifssun  3534  rabexg  4125  pwnss  4138  undifexmid  4172  exmidexmid  4175  exmidsssnc  4182  onintrab2im  4495  ordtriexmidlem  4496  ontr2exmid  4502  ordtri2or2exmidlem  4503  onsucsssucexmid  4504  onsucelsucexmidlem  4506  tfis  4560  nnregexmid  4598  dmmptss  5100  ssimaex  5547  f1oresrab  5650  canth  5796  riotacl  5812  pmvalg  6625  ssfiexmid  6842  domfiexmid  6844  ctssdccl  7076  ctssexmid  7114  genpelxp  7452  ltexprlempr  7549  cauappcvgprlemcl  7594  cauappcvgprlemladd  7599  caucvgprlemcl  7617  caucvgprprlemcl  7645  suplocexprlemex  7663  uzf  9469  supminfex  9535  rpre  9596  ixxf  9834  fzf  9948  expcl2lemap  10467  expclzaplem  10479  expge0  10491  expge1  10492  dvdsflip  11789  infssuzex  11882  infssuzcldc  11884  zsupssdc  11887  gcddvds  11896  uzwodc  11970  nnwosdc  11972  lcmn0cl  12000  phicl2  12146  phimullem  12157  eulerthlemfi  12160  eulerthlemrprm  12161  eulerthlema  12162  eulerthlemh  12163  eulerthlemth  12164  phisum  12172  pcpremul  12225  ennnfonelemg  12336  ennnfonelemh  12337  ctiunctlemuom  12369  epttop  12730  neipsm  12794  cnpfval  12835  blfvalps  13025  blfps  13049  blf  13050  divcnap  13195  cdivcncfap  13227  cnopnap  13234  ivthinclemex  13260  limcdifap  13271  dvfgg  13297  dvidlemap  13300  dvcnp2cntop  13303  dvaddxxbr  13305  dvmulxxbr  13306  dvcoapbr  13311  dvrecap  13317  lgsfcl  13549  lgscl  13555  bdrabexg  13788  subctctexmid  13881