Theorem ssrab2 3323

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

Syntax hints:   /\ wa 104   e. wcel 2203   {cab 2218   {crab 2524   C_ wss 3211

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rab 2529  df-in 3217  df-ss 3224

This theorem is referenced by:  ssrab3  3324  ssrabeq  3326  ifssun  3637  rabexg  4255  pwnss  4272  undifexmid  4306  exmidexmid  4309  exmidsssnc  4316  onintrab2im  4640  ordtriexmidlem  4641  ontr2exmid  4647  ordtri2or2exmidlem  4648  onsucsssucexmid  4649  onsucelsucexmidlem  4651  tfis  4705  nnregexmid  4743  dmmptss  5259  ssimaex  5738  f1oresrab  5842  canth  6001  riotacl  6019  suppssdmg  6449  pmvalg  6893  ssfiexmid  7131  ssfiexmidt  7133  domfiexmid  7135  2omap  7269  ctssdccl  7402  ctssexmid  7441  genpelxp  7826  ltexprlempr  7923  cauappcvgprlemcl  7968  cauappcvgprlemladd  7973  caucvgprlemcl  7991  caucvgprprlemcl  8019  suplocexprlemex  8037  uzf  9856  supminfex  9929  rpre  9993  ixxf  10231  fzf  10346  infssuzex  10593  infssuzcldc  10595  zsupssdc  10598  expcl2lemap  10913  expclzaplem  10925  expge0  10937  expge1  10938  dvdsflip  12537  bitsf  12632  bitsfzolem  12640  gcddvds  12659  uzwodc  12733  nnwosdc  12735  nninfctlemfo  12736  lcmn0cl  12765  phicl2  12911  phimullem  12922  eulerthlemfi  12925  eulerthlemrprm  12926  eulerthlema  12927  eulerthlemh  12928  eulerthlemth  12929  phisum  12938  pcpremul  12991  ballotfilem2  13142  ennnfonelemg  13154  ennnfonelemh  13155  ctiunctlemuom  13187  issubmd  13687  mhmeql  13705  lspf  14537  mplbascoe  14846  mplbasss  14851  epttop  14955  neipsm  15019  cnpfval  15060  blfvalps  15250  blfps  15274  blf  15275  divcnap  15430  cdivcncfap  15469  cnopnap  15476  ivthinclemex  15507  limcdifap  15527  dvfgg  15553  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvcnp2cntop  15564  dvaddxxbr  15566  dvmulxxbr  15567  dvcoapbr  15572  dvrecap  15578  pellexlem3  15847  sgmval2  15852  sgmmul  15864  perfectlem2  15868  lgsfcl  15881  lgscl  15887  lgsquadlem1  15950  lgsquadlem2  15951  incistruhgr  16085  upgrss  16094  usgrss  16172  ushgredgedg  16221  ushgredgedgloop  16223  vtxdfifiun  16292  bdrabexg  16676  pw1map  16769  subctctexmid  16774