Theorem ssrab2 3282

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

Syntax hints:   /\ wa 104   e. wcel 2177   {cab 2192   {crab 2489   C_ wss 3170

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rab 2494  df-in 3176  df-ss 3183

This theorem is referenced by:  ssrab3  3283  ssrabeq  3284  ifssun  3590  rabexg  4195  pwnss  4211  undifexmid  4245  exmidexmid  4248  exmidsssnc  4255  onintrab2im  4574  ordtriexmidlem  4575  ontr2exmid  4581  ordtri2or2exmidlem  4582  onsucsssucexmid  4583  onsucelsucexmidlem  4585  tfis  4639  nnregexmid  4677  dmmptss  5188  ssimaex  5653  f1oresrab  5758  canth  5910  riotacl  5927  pmvalg  6759  ssfiexmid  6988  domfiexmid  6990  ctssdccl  7228  ctssexmid  7267  genpelxp  7644  ltexprlempr  7741  cauappcvgprlemcl  7786  cauappcvgprlemladd  7791  caucvgprlemcl  7809  caucvgprprlemcl  7837  suplocexprlemex  7855  uzf  9671  supminfex  9738  rpre  9802  ixxf  10040  fzf  10154  infssuzex  10398  infssuzcldc  10400  zsupssdc  10403  expcl2lemap  10718  expclzaplem  10730  expge0  10742  expge1  10743  dvdsflip  12237  bitsf  12332  bitsfzolem  12340  gcddvds  12359  uzwodc  12433  nnwosdc  12435  nninfctlemfo  12436  lcmn0cl  12465  phicl2  12611  phimullem  12622  eulerthlemfi  12625  eulerthlemrprm  12626  eulerthlema  12627  eulerthlemh  12628  eulerthlemth  12629  phisum  12638  pcpremul  12691  ennnfonelemg  12849  ennnfonelemh  12850  ctiunctlemuom  12882  issubmd  13381  mhmeql  13399  lspf  14226  mplbascoe  14528  mplbasss  14533  epttop  14637  neipsm  14701  cnpfval  14742  blfvalps  14932  blfps  14956  blf  14957  divcnap  15112  cdivcncfap  15151  cnopnap  15158  ivthinclemex  15189  limcdifap  15209  dvfgg  15235  dvidlemap  15238  dvidrelem  15239  dvidsslem  15240  dvcnp2cntop  15246  dvaddxxbr  15248  dvmulxxbr  15249  dvcoapbr  15254  dvrecap  15260  sgmval2  15531  sgmmul  15543  perfectlem2  15547  lgsfcl  15560  lgscl  15566  lgsquadlem1  15629  lgsquadlem2  15630  incistruhgr  15761  upgrss  15770  bdrabexg  15980  2omap  16071  pw1map  16073  subctctexmid  16078