Theorem ssrab2 3327

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

Syntax hints:   /\ wa 104   e. wcel 2205   {cab 2220   {crab 2526   C_ wss 3214

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rab 2531  df-in 3220  df-ss 3227

This theorem is referenced by:  ssrab3  3328  ssrabeq  3330  ifssun  3641  rabexg  4260  pwnss  4277  undifexmid  4311  exmidexmid  4314  exmidsssnc  4321  onintrab2im  4645  ordtriexmidlem  4646  ontr2exmid  4652  ordtri2or2exmidlem  4653  onsucsssucexmid  4654  onsucelsucexmidlem  4656  tfis  4710  nnregexmid  4748  dmmptss  5264  ssimaex  5743  f1oresrab  5847  canth  6009  riotacl  6027  suppssdmg  6462  pmvalg  6906  ssfiexmid  7144  ssfiexmidt  7146  domfiexmid  7148  2omap  7282  ctssdccl  7415  ctssexmid  7454  genpelxp  7842  ltexprlempr  7939  cauappcvgprlemcl  7984  cauappcvgprlemladd  7989  caucvgprlemcl  8007  caucvgprprlemcl  8035  suplocexprlemex  8053  uzf  9874  supminfex  9947  rpre  10011  ixxf  10250  fzf  10365  infssuzex  10615  infssuzcldc  10617  zsupssdc  10622  expcl2lemap  10937  expclzaplem  10949  expge0  10961  expge1  10962  dvdsflip  12562  bitsf  12657  bitsfzolem  12665  gcddvds  12684  uzwodc  12758  nnwosdc  12760  nninfctlemfo  12761  lcmn0cl  12790  phicl2  12936  phimullem  12947  eulerthlemfi  12950  eulerthlemrprm  12951  eulerthlema  12952  eulerthlemh  12953  eulerthlemth  12954  phisum  12963  pcpremul  13016  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemiex  13188  ballotfilem7  13223  ballotfilemth  13225  ennnfonelemg  13238  ennnfonelemh  13239  ctiunctlemuom  13271  issubmd  13729  mhmeql  13747  lspf  14663  mplbascoe  14972  mplbasss  14977  epttop  15081  neipsm  15145  cnpfval  15186  blfvalps  15376  blfps  15400  blf  15401  divcnap  15556  cdivcncfap  15595  cnopnap  15602  ivthinclemex  15633  limcdifap  15653  dvfgg  15679  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvcnp2cntop  15690  dvaddxxbr  15692  dvmulxxbr  15693  dvcoapbr  15698  dvrecap  15704  pellexlem3  15973  sgmval2  15978  sgmmul  15990  perfectlem2  15994  lgsfcl  16007  lgscl  16013  lgsquadlem1  16076  lgsquadlem2  16077  incistruhgr  16211  upgrss  16220  usgrss  16298  ushgredgedg  16347  ushgredgedgloop  16349  vtxdfifiun  16418  bdrabexg  16802  pw1map  16895  subctctexmid  16900