MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssrab2 Structured version   Unicode version

Theorem ssrab2 3570
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
StepHypRef Expression
1 df-rab 2802 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3569 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3519 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    e. wcel 1804   {cab 2428   {crab 2797    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-in 3468  df-ss 3475
This theorem is referenced by:  ssrabeq  3571  iinrab2  4378  riinrab  4391  rabexg  4587  pwnss  4602  frminex  4849  wereu2  4866  dmmptss  5493  ssimaex  5923  f1oresrab  6048  fnsuppresOLD  6116  weniso  6235  canth  6239  riotacl  6257  riotassuniOLD  6279  onminesb  6618  onminsb  6619  onintrab  6621  onnminsb  6624  onminex  6627  tfis  6674  omsson  6689  suppssdm  6916  fnsuppres  6929  oawordeulem  7205  oeeulem  7252  nnawordex  7288  pmvalg  7433  fineqvlem  7736  ordtypelem2  7947  ordtypelem3  7948  ordtypelem4  7949  ordtypelem6  7951  hartogs  7972  wemapso2OLD  7980  wemapso2lem  7981  card2on  7983  wdom2d  8009  oemapvali  8106  wemapwe  8142  wemapweOLD  8143  tz9.12lem1  8208  tz9.12lem3  8210  rankf  8215  cplem1  8310  cardf2  8327  cardid2  8337  cardmin2  8382  acni3  8431  dfac2a  8513  cofsmo  8652  coftr  8656  fin2i2  8701  isfin2-2  8702  enfin2i  8704  fin23lem28  8723  fin23lem30  8725  isf32lem5  8740  isf32lem6  8741  isf32lem7  8742  isf32lem8  8743  fin1a2lem11  8793  fin1a2lem12  8794  hsmexlem4  8812  hsmexlem5  8813  hsmexlem6  8814  axdc3lem4  8836  ac6num  8862  ac6  8863  zorn2lem1  8879  zorn2lem3  8881  zorn2lem4  8882  zorn2lem5  8883  ondomon  8941  alephval2  8950  pwfseqlem1  9039  pwfseqlem3  9041  wunccl  9125  tskmcl  9222  0nnq  9305  elpqn  9306  infm3  10508  infmrcl  10528  uzf  11093  nnwos  11158  supminf  11178  zsupss  11180  rpnnen1lem1  11217  rpnnen1lem2  11218  rpnnen1lem3  11219  rpnnen1lem5  11221  rpre  11235  ixxf  11548  fzf  11685  flval3  11930  rabssnn0fi  12074  expge0  12181  expge1  12182  hashbclem  12480  sqrlem3  13057  sqrlem5  13059  rlimrege0  13381  incexc2  13629  divalglem2  13930  divalglem5  13932  divalglem8  13935  bitsf  13954  bitsfzolem  13961  sadadd2lem  13986  sadadd3  13988  sadcl  13989  smupf  14005  smuval2  14009  smupvallem  14010  smucl  14011  smueqlem  14017  gcdcllem3  14028  bezoutlem2  14054  bezoutlem3  14055  maxprmfct  14131  phicl2  14175  phibnd  14178  hashdvds  14182  phiprmpw  14183  phimullem  14186  eulerthlem2  14189  eulerth  14190  odzcllem  14196  odzdvds  14199  pclem  14239  infpn2  14308  prmreclem1  14311  prmreclem2  14312  prmreclem3  14313  prmreclem4  14314  prmreclem5  14315  4sqlem13  14352  4sqlem14  14353  4sqlem17  14356  4sqlem18  14357  vdwnnlem3  14392  hashbccl  14398  ramcl2lem  14404  ramtcl  14405  ramtcl2  14406  ramtub  14407  prdsds  14738  imasdsval2  14790  mrcflem  14880  isacs1i  14931  wunnat  15199  dmcoass  15267  lublecl  15493  lubid  15494  gsumval1  15778  issubmd  15854  mhmeql  15869  nmzsubg  16116  nmznsg  16119  conjnmz  16174  conjnmzb  16175  gastacl  16221  cntzval  16233  cntzssv  16240  symgsssg  16366  symgfisg  16367  pmtrdifellem4  16378  odlem1  16433  odlem2  16437  odngen  16471  gexlem1  16473  gexlem2  16476  sylow1lem2  16493  sylow1lem3  16494  sylow1lem4  16495  sylow1lem5  16496  sylow2alem2  16512  sylow2a  16513  sylow2blem3  16516  sylow3lem2  16522  oddvdssubg  16735  cyggex2  16773  ablfacrplem  16990  ablfacrp2  16992  ablfac1eu  16998  pgpfaclem1  17006  ablfaclem2  17011  ablfaclem3  17012  lssacs  17487  lspf  17494  lspsolvlem  17662  lbsextlem2  17679  lbsextlem3  17680  lbsextlem4  17681  rrgeq0  17812  rrgss  17815  asplss  17852  aspsubrg  17854  psrbagconf1o  17900  psrass1lem  17903  psrdi  17935  psrdir  17936  psrass23l  17937  psrass23  17939  resspsrmul  17946  mplbas  17960  mplbasOLD  17962  mplbasss  17965  mplsubglem  17967  mplsubglemOLD  17969  mplsubrglem  17974  mplsubrglemOLD  17975  mplmonmul  18000  psropprmul  18153  coe1mul2lem2  18183  cygznlem2a  18479  psgnghm  18489  ocvfval  18570  ocvval  18571  dsmmbase  18639  dsmmval2  18640  dsmmsubg  18647  frlmsslsp  18702  frlmsslspOLD  18703  scmatlss  18900  smadiadet  19045  pmatcoe1fsupp  19075  cpmatsubgpmat  19094  fctop  19378  cctop  19380  ppttop  19381  epttop  19383  clscld  19421  mretopd  19466  neips  19487  neiptopnei  19506  ordtbaslem  19562  ordtuni  19564  ordtcld1  19571  ordtcld2  19572  cnpfval  19608  iscnp2  19613  cmpcov2  19763  cmpsublem  19772  tgcmp  19774  hauscmplem  19779  concompcld  19808  1stcfb  19819  2ndc1stc  19825  2ndcdisj  19830  finlocfin  19894  kgentopon  19912  xkotf  19959  txkgen  20026  xkococnlem  20033  imastopn  20094  kqffn  20099  opnfbas  20216  flimfnfcls  20402  alexsubALT  20424  ptcmplem1  20425  ptcmplem2  20426  ptcmplem3  20427  symgtgp  20473  tgpconcompeqg  20483  tgpconcomp  20484  ghmcnp  20486  tsmsfbas  20499  eltsms  20504  utoptop  20610  utopbas  20611  imasdsf1olem  20749  blfvalps  20759  blfps  20782  blf  20783  blcld  20881  nmoffn  21091  nmofval  21094  nmogelb  21096  nmolb  21097  nmof  21099  icccmplem1  21200  icccmplem2  21201  icccmplem3  21202  ishtpy  21345  clsocv  21563  rrxnm  21696  rrxf  21701  minveclem3b  21716  minveclem4  21720  ivthlem1  21736  ivthlem2  21737  ivthlem3  21738  ovolcl  21762  ovollb  21763  ovolgelb  21764  ovolge0  21765  ovolsslem  21768  ovolshftlem1  21793  ovolshft  21795  ovolscalem1  21797  ovolscalem2  21798  ovolsca  21799  ovolicc2lem3  21803  ovolicc2lem4  21804  ovolicc2lem5  21805  ovolicc2  21806  shftmbl  21822  iundisj  21831  dyadmax  21880  dyadmbllem  21881  dyadmbl  21882  opnmbllem  21883  iblmbf  22047  mdegmullem  22351  uc1pval  22413  mon1pval  22415  elqaalem1  22587  elqaalem3  22589  aannenlem2  22597  aalioulem2  22601  radcnvcl  22684  radcnvlt1  22685  radcnvle  22687  abelthlem4  22701  abelthlem6  22703  abelthlem9  22707  abelth  22708  atancn  23139  ftalem3  23220  ftalem4  23221  ftalem5  23222  efnnfsumcl  23248  isppw  23260  sgmval2  23289  efchtdvds  23305  sqff1o  23328  dvdsflip  23330  fsumdvdsdiaglem  23331  fsumdvdsdiag  23332  fsumdvdscom  23333  musum  23339  muinv  23341  dvdsmulf1o  23342  fsumdvdsmul  23343  sgmmul  23348  ppiub  23351  vmasum  23363  logfac2  23364  perfectlem2  23377  lgsfcl2  23449  lgsfcl  23451  lgscl  23457  lgsquadlem1  23501  lgsquadlem2  23502  rpvmasumlem  23544  rpvmasum2  23569  dchrisum0re  23570  dchrisum0lema  23571  dchrisum0lem1b  23572  dchrisum0lem1  23573  dchrisum0lem2a  23574  dchrisum0lem2  23575  dchrisum0lem3  23576  dchrisum0  23577  mudivsum  23587  mulogsum  23589  mulog2sumlem2  23592  vmalogdivsum2  23595  logsqvma  23599  logsqvma2  23600  selberglem3  23604  selberg  23605  selberg34r  23628  pntsval2  23633  pntrlog2bndlem1  23634  pntlem3  23666  tglnunirn  23807  tglnssp  23811  axcontlem2  24140  axcontlem7  24145  axcontlem8  24146  axcontlem10  24148  umgrass  24191  umgran0  24192  umisuhgra  24199  usgrass  24233  uslisushgra  24235  usgrares1  24282  usgrafilem1  24283  nbgrassvt  24305  nbgraf1olem1  24313  cusgrares  24344  hashwwlkext  24618  clwwlksswrd  24649  vdgrun  24773  vdgrfiun  24774  konigsberg  24859  frisusgranb  24869  frgrawopreg1  24922  frgrawopreg2  24923  ocsh  26073  spancl  26126  shsval2i  26177  ococin  26198  chsupid  26202  speccl  26690  atssch  27134  hatomistici  27153  chpssati  27154  iundisjf  27320  fcobijfs  27421  fpwrelmap  27428  iundisjfi  27473  locfinreflem  27716  esumpinfval  27952  sigagensiga  28014  measvuni  28058  imambfm  28106  dya2iocuni  28127  oms0  28139  omsmon  28140  oddpwdc  28166  eulerpartlem1  28179  eulerpartlemt  28183  eulerpartgbij  28184  eulerpartlemmf  28187  eulerpartlemgvv  28188  eulerpartlemgh  28190  eulerpartlemgs2  28192  ballotlem2  28300  ballotlemfc0  28304  ballotlemfcc  28305  ballotlemfmpn  28306  ballotlemiex  28313  ballotlemsup  28316  ballotlem7  28347  ballotth  28349  lgamucov  28453  lgamucov2  28454  subfacp1lem3  28499  subfacp1lem5  28501  subfacp1lem6  28502  erdszelem2  28509  conpcon  28553  cvmliftmolem2  28600  cvmliftlem15  28616  cvmlift2lem12  28632  snmlff  28647  tfisg  29259  wfisg  29264  frinsg  29300  wlimss  29360  sltval2  29391  nodenselem4  29419  nobndlem5  29431  nofulllem5  29441  rankeq1o  29803  fin2so  30015  opnmbllem0  30025  mblfinlem1  30026  mblfinlem2  30027  ismblfin  30030  mbfposadd  30037  cnambfre  30038  finminlem  30111  fnessref  30150  neibastop1  30152  neibastop2lem  30153  cover2  30179  indexa  30199  fdc  30213  sstotbnd2  30245  sstotbnd3  30247  igenidl  30435  prnc  30439  mzpindd  30653  fiphp3d  30728  rencldnfilem  30729  irrapx1  30739  pellexlem3  30742  pellfundre  30792  pellfundge  30793  pellfundlb  30795  pellfundglb  30796  jm2.22  30912  jm2.23  30913  rpnnen3  30949  fglmod  30994  pwssplit4  31010  pwfi2f1o  31019  hbtlem6  31053  dgraalem  31070  dgraaub  31073  itgocn  31089  rgspncl  31094  phisum  31135  lcmcllem  31178  lcmn0cl  31179  lcmledvds  31181  limcperiod  31542  sumnnodd  31544  cncfshift  31583  cncfperiod  31588  ioodvbdlimc1lem1  31632  stoweidlem14  31685  stoweidlem34  31705  stoweidlem44  31715  stoweidlem50  31721  stoweidlem51  31722  stoweidlem52  31723  stoweidlem57  31728  stoweidlem59  31730  fourierdlem19  31797  fourierdlem20  31798  fourierdlem25  31803  fourierdlem31  31809  fourierdlem37  31815  fourierdlem42  31820  fourierdlem51  31829  fourierdlem54  31832  fourierdlem64  31842  fourierdlem79  31857  rabsubmgmd  32317  mgmhmeql  32329  oddibas  32338  2zlidl  32450  2zrngbas  32452  2zrng0  32454  bnj21  33503  bnj110  33649  bnj1204  33801  bnj1311  33813  bj-rabtr  34245  bj-rabtrAUTO  34247  bj-cmnssmnd  34392  bj-vecssmod  34399  bj-rrvecssvec  34406  toycom  34438  lkrlss  34560  atlatmstc  34784  atlatle  34785  glbconN  34841  linepsubN  35216  pmapssat  35223  pmaple  35225  pmapsub  35232  paddssat  35278  diass  36509  diaglbN  36522  diaintclN  36525  diassdvaN  36527  docaclN  36591  dibglbN  36633  dibintclN  36634  diclspsn  36661  dihglblem2N  36761  dih1dimatlem  36796  dihglb2  36809  dochval2  36819  dochcl  36820  dochvalr  36824  doch2val2  36831  dochss  36832  dochocss  36833  lclkr  37000  lclkrs  37006  lcdvbase  37060  lcdvbasess  37061  mapdunirnN  37117
  Copyright terms: Public domain W3C validator