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  6938  ssfiexmid  7184  ssfiexmidt  7186  domfiexmid  7188  2omap  7324  ctssdccl  7457  ctssexmid  7496  genpelxp  7884  ltexprlempr  7981  cauappcvgprlemcl  8026  cauappcvgprlemladd  8031  caucvgprlemcl  8049  caucvgprprlemcl  8077  suplocexprlemex  8095  uzf  9939  supminfex  10012  rpre  10077  ixxf  10316  fzf  10431  infssuzex  10682  infssuzcldc  10684  zsupssdc  10689  expcl2lemap  11008  expclzaplem  11020  expge0  11032  expge1  11033  dvdsflip  12642  bitsf  12737  bitsfzolem  12745  gcddvds  12764  uzwodc  12838  nnwosdc  12840  nninfctlemfo  12841  lcmn0cl  12870  phicl2  13020  phimullem  13031  eulerthlemfi  13034  eulerthlemrprm  13035  eulerthlema  13036  eulerthlemh  13037  eulerthlemth  13038  phisum  13047  pcpremul  13100  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemiex  13301  ballotfilem7  13336  ballotfilemth  13338  ennnfonelemg  13351  ennnfonelemh  13352  ctiunctlemuom  13384  issubmd  13839  mhmeql  13857  cntzssv  14159  lspf  14834  asplss  15124  aspsubrg  15126  psrbagmax  15183  psrass1filem  15186  psrdifi  15211  psrdirfi  15212  mplbas  15223  epttop  15333  neipsm  15397  cnpfval  15438  blfvalps  15628  blfps  15652  blf  15653  divcnap  15808  cdivcncfap  15847  cnopnap  15854  ivthinclemex  15885  limcdifap  15905  dvfgg  15931  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvcnp2cntop  15942  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvrecap  15956  pellexlem3  16248  efnnfsumcl  16256  sgmval2  16270  efchtqdvds  16282  sgmmul  16307  ppiqub  16310  perfectlem2  16317  lgsfcl  16349  lgscl  16355  lgsquadlem1  16418  lgsquadlem2  16419  incistruhgr  16553  upgrss  16562  usgrss  16640  ushgredgedg  16689  ushgredgedgloop  16691  vtxdfifiun  16760  bdrabexg  17154  pw1map  17247  subctctexmid  17252  stnot  17261  wexmiddc  17264