Theorem ssrab2 3309

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

Syntax hints:   /\ wa 104   e. wcel 2200   {cab 2215   {crab 2512   C_ wss 3197

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-in 3203  df-ss 3210

This theorem is referenced by:  ssrab3  3310  ssrabeq  3311  ifssun  3617  rabexg  4227  pwnss  4243  undifexmid  4277  exmidexmid  4280  exmidsssnc  4287  onintrab2im  4610  ordtriexmidlem  4611  ontr2exmid  4617  ordtri2or2exmidlem  4618  onsucsssucexmid  4619  onsucelsucexmidlem  4621  tfis  4675  nnregexmid  4713  dmmptss  5225  ssimaex  5695  f1oresrab  5800  canth  5952  riotacl  5970  pmvalg  6806  ssfiexmid  7038  domfiexmid  7040  ctssdccl  7278  ctssexmid  7317  genpelxp  7698  ltexprlempr  7795  cauappcvgprlemcl  7840  cauappcvgprlemladd  7845  caucvgprlemcl  7863  caucvgprprlemcl  7891  suplocexprlemex  7909  uzf  9725  supminfex  9792  rpre  9856  ixxf  10094  fzf  10208  infssuzex  10453  infssuzcldc  10455  zsupssdc  10458  expcl2lemap  10773  expclzaplem  10785  expge0  10797  expge1  10798  dvdsflip  12362  bitsf  12457  bitsfzolem  12465  gcddvds  12484  uzwodc  12558  nnwosdc  12560  nninfctlemfo  12561  lcmn0cl  12590  phicl2  12736  phimullem  12747  eulerthlemfi  12750  eulerthlemrprm  12751  eulerthlema  12752  eulerthlemh  12753  eulerthlemth  12754  phisum  12763  pcpremul  12816  ennnfonelemg  12974  ennnfonelemh  12975  ctiunctlemuom  13007  issubmd  13507  mhmeql  13525  lspf  14353  mplbascoe  14655  mplbasss  14660  epttop  14764  neipsm  14828  cnpfval  14869  blfvalps  15059  blfps  15083  blf  15084  divcnap  15239  cdivcncfap  15278  cnopnap  15285  ivthinclemex  15316  limcdifap  15336  dvfgg  15362  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvcnp2cntop  15373  dvaddxxbr  15375  dvmulxxbr  15376  dvcoapbr  15381  dvrecap  15387  sgmval2  15658  sgmmul  15670  perfectlem2  15674  lgsfcl  15687  lgscl  15693  lgsquadlem1  15756  lgsquadlem2  15757  incistruhgr  15890  upgrss  15899  usgrss  15975  ushgredgedg  16024  ushgredgedgloop  16026  bdrabexg  16269  2omap  16359  pw1map  16361  subctctexmid  16366