Theorem ssrab2 3333

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

This proof depends on syntax axioms:   /\ wa 104   e. wcel 2209   {cab 2224   {crab 2532   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-in 3226  df-ss 3233

This theorem is used by:  ssrab3  3334  ssrabeq  3336  ifssun  3655  rabexg  4281  pwnss  4298  undifexmid  4332  exmidexmid  4335  exmidsssnc  4342  onintrab2im  4667  ordtriexmidlem  4668  ontr2exmid  4674  ordtri2or2exmidlem  4675  onsucsssucexmid  4676  onsucelsucexmidlem  4678  tfis  4732  nnregexmid  4770  dmmptss  5287  ssimaex  5767  f1oresrab  5876  canth  6039  riotacl  6057  suppssdmg  6493  pmvalg  6937  ssfiexmid  7182  ssfiexmidt  7184  domfiexmid  7186  2omap  7324  ctssdccl  7457  ctssexmid  7496  genpelxp  7884  ltexprlempr  7981  cauappcvgprlemcl  8026  cauappcvgprlemladd  8031  caucvgprlemcl  8049  caucvgprprlemcl  8077  suplocexprlemex  8095  uzf  9940  supminfex  10013  rpre  10078  ixxf  10317  fzf  10432  infssuzex  10683  infssuzcldc  10685  zsupssdc  10690  expcl2lemap  11009  expclzaplem  11021  expge0  11033  expge1  11034  dvdsflip  12643  bitsf  12738  bitsfzolem  12746  gcddvds  12765  uzwodc  12839  nnwosdc  12841  nninfctlemfo  12842  lcmn0cl  12871  phicl2  13021  phimullem  13032  eulerthlemfi  13035  eulerthlemrprm  13036  eulerthlema  13037  eulerthlemh  13038  eulerthlemth  13039  phisum  13048  pcpremul  13101  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemiex  13302  ballotfilem7  13337  ballotfilemth  13339  ennnfonelemg  13352  ennnfonelemh  13353  ctiunctlemuom  13385  issubmd  13840  mhmeql  13858  cntzssv  14160  lspf  14835  asplss  15125  aspsubrg  15127  psrass1filem  15177  psrdifi  15202  psrdirfi  15203  mplbascoe  15207  mplbasss  15212  epttop  15316  neipsm  15380  cnpfval  15421  blfvalps  15611  blfps  15635  blf  15636  divcnap  15791  cdivcncfap  15830  cnopnap  15837  ivthinclemex  15868  limcdifap  15888  dvfgg  15914  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvcnp2cntop  15925  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  dvrecap  15939  pellexlem3  16231  efnnfsumcl  16239  sgmval2  16253  efchtqdvds  16265  sgmmul  16290  ppiqub  16293  perfectlem2  16300  lgsfcl  16332  lgscl  16338  lgsquadlem1  16401  lgsquadlem2  16402  incistruhgr  16536  upgrss  16545  usgrss  16623  ushgredgedg  16672  ushgredgedgloop  16674  vtxdfifiun  16743  bdrabexg  17137  pw1map  17230  subctctexmid  17235  stnot  17244  wexmiddc  17247