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

Theorem ssrab2 3526
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 2758 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3525 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3474 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 375    e. wcel 1898   {cab 2448   {crab 2753    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-in 3423  df-ss 3430
This theorem is referenced by:  ssrabeq  3527  iinrab2  4355  riinrab  4368  rabexg  4567  pwnss  4582  frminex  4833  wereu2  4850  dmmptss  5350  wfisg  5434  ssimaex  5953  f1oresrab  6079  weniso  6270  canth  6274  riotacl  6291  riotassuni  6313  onminesb  6652  onminsb  6653  onintrab  6655  onnminsb  6658  onminex  6661  tfis  6708  omsson  6723  suppssdm  6954  fnsuppres  6969  oawordeulem  7281  oeeulem  7328  nnawordex  7364  pmvalg  7509  fineqvlem  7812  ordtypelem2  8060  ordtypelem3  8061  ordtypelem4  8062  ordtypelem6  8064  hartogs  8085  wemapso2lem  8093  card2on  8095  wdom2d  8121  oemapvali  8215  wemapwe  8228  tz9.12lem1  8284  tz9.12lem3  8286  rankf  8291  cplem1  8386  cardf2  8403  cardid2  8413  cardmin2  8458  acni3  8504  dfac2a  8586  cofsmo  8725  coftr  8729  fin2i2  8774  isfin2-2  8775  enfin2i  8777  fin23lem28  8796  fin23lem30  8798  isf32lem5  8813  isf32lem6  8814  isf32lem7  8815  isf32lem8  8816  fin1a2lem11  8866  fin1a2lem12  8867  hsmexlem4  8885  hsmexlem5  8886  hsmexlem6  8887  axdc3lem4  8909  ac6num  8935  ac6  8936  zorn2lem1  8952  zorn2lem3  8954  zorn2lem4  8955  zorn2lem5  8956  ondomon  9014  alephval2  9023  pwfseqlem1  9109  pwfseqlem3  9111  wunccl  9195  tskmcl  9292  0nnq  9375  elpqn  9376  fiminre  10583  infm3  10596  infmrclOLD  10621  uzf  11191  nnwos  11255  supminf  11279  supminfOLD  11280  zsupss  11282  rpnnen1lem1  11319  rpnnen1lem2  11320  rpnnen1lem3  11321  rpnnen1lem5  11323  rpre  11337  ixxf  11674  fzf  11817  flval3  12082  rabssnn0fi  12230  expge0  12340  expge1  12341  hashbclem  12648  sqrlem3  13357  sqrlem5  13359  rlimrege0  13692  incexc2  13945  divalglem2  14422  divalglem2OLD  14423  divalglem5OLD  14425  divalglem5  14426  divalglem8  14429  bitsf  14449  bitsfzolem  14456  bitsfzolemOLD  14457  sadadd2lem  14482  sadadd3  14484  sadcl  14485  smupf  14501  smuval2  14505  smupvallem  14506  smucl  14507  smueqlem  14513  gcdcllem3  14524  bezoutlem2OLD  14553  bezoutlem3OLD  14554  bezoutlem2  14556  bezoutlem3  14557  lcmcllem  14610  lcmn0cl  14611  lcmledvds  14613  lcmscllemOLD  14631  lcmsnnOLD  14632  lcmsledvdsOLD  14634  lcmfval  14640  lcmfvalOLD  14644  lcmfcllem  14647  lcmfn0cl  14648  lcmfledvds  14654  maxprmfct  14701  phicl2  14765  phibnd  14768  hashdvds  14772  phiprmpw  14773  phimullem  14776  eulerthlem2  14779  eulerth  14780  odzcllem  14786  odzdvds  14789  odzcllemOLD  14792  odzdvdsOLD  14795  pclem  14837  infpn2  14906  prmreclem1  14909  prmreclem2  14910  prmreclem3  14911  prmreclem4  14912  prmreclem5  14913  4sqlem13OLD  14950  4sqlem14OLD  14951  4sqlem17OLD  14954  4sqlem18OLD  14955  4sqlem13  14956  4sqlem14  14957  4sqlem17  14960  4sqlem18  14961  vdwnnlem3  14996  hashbccl  15004  ramcl2lem  15011  ramcl2lemOLD  15012  ramtcl  15013  ramtclOLD  15014  ramtcl2  15015  ramtcl2OLD  15016  ramtub  15017  ramtubOLD  15018  prmordvdslcmsOLDOLD  15070  prmgaplem3  15072  prmgaplem4  15073  prdsds  15411  imasdsval2  15466  imasdsval2OLD  15478  mrcflem  15561  isacs1i  15612  wunnat  15910  dmcoass  16010  lublecl  16284  lubid  16285  gsumval1  16569  issubmd  16645  mhmeql  16660  nmzsubg  16907  nmznsg  16910  conjnmz  16965  conjnmzb  16966  gastacl  17012  cntzval  17024  cntzssv  17031  symgsssg  17157  symgfisg  17158  pmtrdifellem4  17169  odlem1  17230  odlem1OLD  17233  odlem2  17237  odlem2OLD  17253  odngen  17275  gexlem1  17277  gexlem1OLD  17279  gexlem2  17282  gexlem2OLD  17285  sylow1lem2  17300  sylow1lem3  17301  sylow1lem4  17302  sylow1lem5  17303  sylow2alem2  17319  sylow2a  17320  sylow2blem3  17323  sylow3lem2  17329  oddvdssubg  17542  cyggex2  17580  ablfacrplem  17747  ablfacrp2  17749  ablfac1eu  17755  pgpfaclem1  17763  ablfaclem2  17768  ablfaclem3  17769  lssacs  18239  lspf  18246  lspsolvlem  18414  lbsextlem2  18431  lbsextlem3  18432  lbsextlem4  18433  rrgeq0  18563  rrgss  18565  asplss  18602  aspsubrg  18604  psrbagconf1o  18647  psrass1lem  18650  psrdi  18679  psrdir  18680  psrass23l  18681  psrass23  18683  resspsrmul  18690  mplbas  18702  mplbasss  18705  mplsubglem  18707  mplsubrglem  18712  mplmonmul  18737  psropprmul  18880  coe1mul2lem2  18910  cygznlem2a  19187  psgnghm  19197  ocvfval  19278  ocvval  19279  dsmmbase  19347  dsmmval2  19348  dsmmsubg  19355  frlmsslsp  19403  scmatlss  19599  smadiadet  19744  pmatcoe1fsupp  19774  cpmatsubgpmat  19793  fctop  20068  cctop  20070  ppttop  20071  epttop  20073  clscld  20111  mretopd  20157  neips  20178  neiptopnei  20197  ordtbaslem  20253  ordtuni  20255  ordtcld1  20262  ordtcld2  20263  cnpfval  20299  iscnp2  20304  cmpcov2  20454  cmpsublem  20463  tgcmp  20465  hauscmplem  20470  concompcld  20498  1stcfb  20509  2ndc1stc  20515  2ndcdisj  20520  finlocfin  20584  kgentopon  20602  xkotf  20649  txkgen  20716  xkococnlem  20723  imastopn  20784  kqffn  20789  opnfbas  20906  flimfnfcls  21092  alexsubALT  21115  ptcmplem1  21116  ptcmplem2  21117  ptcmplem3  21118  symgtgp  21165  tgpconcompeqg  21175  tgpconcomp  21176  ghmcnp  21178  tsmsfbas  21191  eltsms  21196  utoptop  21298  utopbas  21299  imasdsf1olem  21437  blfvalps  21447  blfps  21470  blf  21471  blcld  21569  nmoffn  21765  nmofval  21768  nmogelb  21770  nmolb  21771  nmof  21773  nmoffnOLD  21786  nmofvalOLD  21787  nmogelbOLD  21789  nmolbOLD  21790  nmofOLD  21791  icccmplem1  21889  icccmplem2  21890  icccmplem3  21891  ishtpy  22052  clsocv  22270  rrxnm  22399  rrxf  22404  minveclem3b  22419  minveclem4  22423  minveclem3bOLD  22431  minveclem4OLD  22435  ivthlem1  22451  ivthlem2  22452  ivthlem3  22453  ovolcl  22480  ovollb  22481  ovolgelb  22482  ovolge0  22483  ovolsslem  22486  ovolshftlem1  22511  ovolshft  22513  ovolscalem1  22515  ovolscalem2  22516  ovolsca  22517  ovolicc2lem3  22521  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  ovolicc2lem5  22524  ovolicc2  22525  shftmbl  22541  iundisj  22550  dyadmax  22605  dyadmbllem  22606  dyadmbl  22607  opnmbllem  22608  iblmbf  22774  mdegmullem  23076  uc1pval  23139  mon1pval  23141  elqaalem1  23321  elqaalem3  23323  elqaalem1OLD  23324  elqaalem3OLD  23326  aannenlem2  23334  aalioulem2  23338  radcnvcl  23421  radcnvlt1  23422  radcnvle  23424  abelthlem4  23438  abelthlem6  23440  abelthlem9  23444  abelth  23445  atancn  23911  lgamucov  24012  lgamucov2  24013  ftalem3  24048  ftalem4  24049  ftalem5  24050  ftalem4OLD  24051  ftalem5OLD  24052  efnnfsumcl  24078  isppw  24090  sgmval2  24119  efchtdvds  24135  sqff1o  24158  dvdsflip  24160  fsumdvdsdiaglem  24161  fsumdvdsdiag  24162  fsumdvdscom  24163  musum  24169  muinv  24171  dvdsmulf1o  24172  fsumdvdsmul  24173  sgmmul  24178  ppiub  24181  vmasum  24193  logfac2  24194  perfectlem2  24207  lgsfcl2  24279  lgsfcl  24281  lgscl  24287  lgsquadlem1  24331  lgsquadlem2  24332  rpvmasumlem  24374  rpvmasum2  24399  dchrisum0re  24400  dchrisum0lema  24401  dchrisum0lem1b  24402  dchrisum0lem1  24403  dchrisum0lem2a  24404  dchrisum0lem2  24405  dchrisum0lem3  24406  dchrisum0  24407  mudivsum  24417  mulogsum  24419  mulog2sumlem2  24422  vmalogdivsum2  24425  logsqvma  24429  logsqvma2  24430  selberglem3  24434  selberg  24435  selberg34r  24458  pntsval2  24463  pntrlog2bndlem1  24464  pntlem3  24496  tglnunirn  24642  tglnssp  24646  axcontlem2  25044  axcontlem7  25049  axcontlem8  25050  axcontlem10  25052  umgrass  25095  umgran0  25096  umisuhgra  25103  usgrass  25137  uslisushgra  25139  usgrares1  25187  usgrafilem1  25188  nbgrassvt  25210  nbgraf1olem1  25218  cusgrares  25249  hashwwlkext  25523  clwwlksswrd  25554  vdgrun  25678  vdgrfiun  25679  konigsberg  25764  frisusgranb  25774  frgrawopreg1  25827  frgrawopreg2  25828  ocsh  26985  spancl  27038  shsval2i  27089  ococin  27110  chsupid  27114  speccl  27601  atssch  28045  hatomistici  28064  chpssati  28065  iundisjf  28248  aciunf1  28314  fcobijfs  28360  fpwrelmap  28367  iundisjfi  28421  locfinreflem  28716  esumrnmpt2  28938  esumpinfval  28943  sigagensiga  29012  ldgenpisyslem1  29034  ldgenpisys  29037  measvuni  29085  imambfm  29133  dya2iocuni  29154  omscl  29168  omsclOLD  29172  oms0  29174  omsmon  29175  omssubadd  29177  oms0OLD  29178  omsmonOLD  29179  omssubaddOLD  29181  carsgcl  29185  oddpwdc  29236  eulerpartlem1  29249  eulerpartlemt  29253  eulerpartgbij  29254  eulerpartlemmf  29257  eulerpartlemgvv  29258  eulerpartlemgh  29260  eulerpartlemgs2  29262  ballotlem2  29370  ballotlemfc0  29374  ballotlemfcc  29375  ballotlemfmpn  29376  ballotlemiex  29383  ballotlemsup  29386  ballotlem7  29417  ballotth  29419  ballotlemiexOLD  29421  ballotlemsupOLD  29424  ballotlem7OLD  29455  ballotthOLD  29457  bnj21  29572  bnj110  29718  bnj1204  29870  bnj1311  29882  subfacp1lem3  29954  subfacp1lem5  29956  subfacp1lem6  29957  erdszelem2  29964  conpcon  30007  cvmliftmolem2  30054  cvmliftlem15  30070  cvmlift2lem12  30086  snmlff  30101  tfisg  30506  frinsg  30532  wlimss  30561  sltval2  30592  nodenselem4  30622  nobndlem5  30634  nofulllem5  30644  rankeq1o  30987  finminlem  31023  fnessref  31062  neibastop1  31064  neibastop2lem  31065  bj-rabtr  31578  bj-rabtrALTALT  31580  bj-rabtrAUTO  31581  bj-cmnssmnd  31736  bj-vecssmod  31743  bj-rrvecssvec  31750  icoreresf  31800  phpreu  31974  fin2so  31977  poimirlem26  32011  poimirlem31  32016  poimirlem32  32017  opnmbllem0  32021  mblfinlem1  32022  mblfinlem2  32023  ismblfin  32026  mbfposadd  32033  cnambfre  32034  cover2  32085  indexa  32105  fdc  32119  sstotbnd2  32151  sstotbnd3  32153  igenidl  32341  prnc  32345  toycom  32584  lkrlss  32706  atlatmstc  32930  atlatle  32931  glbconN  32987  linepsubN  33362  pmapssat  33369  pmaple  33371  pmapsub  33378  paddssat  33424  diass  34655  diaglbN  34668  diaintclN  34671  diassdvaN  34673  docaclN  34737  dibglbN  34779  dibintclN  34780  diclspsn  34807  dihglblem2N  34907  dih1dimatlem  34942  dihglb2  34955  dochval2  34965  dochcl  34966  dochvalr  34970  doch2val2  34977  dochss  34978  dochocss  34979  lclkr  35146  lclkrs  35152  lcdvbase  35206  lcdvbasess  35207  mapdunirnN  35263  mzpindd  35633  fiphp3d  35707  rencldnfilem  35708  irrapx1  35717  pellexlem3  35720  pellfundre  35774  pellfundge  35775  pellfundlb  35777  pellfundglb  35778  jm2.22  35895  jm2.23  35896  rpnnen3  35932  fglmod  35976  pwssplit4  35992  pwfi2f1o  35999  hbtlem6  36033  dgraalem  36052  dgraalemOLD  36053  dgraaub  36058  dgraaubOLD  36059  itgocn  36075  rgspncl  36080  phisum  36121  binomcxplemdvbinom  36746  binomcxplemcvg  36747  binomcxplemnotnn0  36749  uzwo4  37430  disjf1o  37504  fsumsupp0  37695  limcperiod  37746  sumnnodd  37748  cncfshift  37789  cncfperiod  37794  ioodvbdlimc1lem1  37841  ioodvbdlimc1lem1OLD  37843  dvnprodlem1  37859  dvnprodlem2  37860  stoweidlem14  37912  stoweidlem34  37933  stoweidlem44  37943  stoweidlem50  37949  stoweidlem51  37950  stoweidlem52  37951  stoweidlem57  37956  stoweidlem59  37958  fourierdlem19  38026  fourierdlem20  38027  fourierdlem25  38032  fourierdlem31  38038  fourierdlem31OLD  38039  fourierdlem37  38045  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem51  38059  fourierdlem54  38062  fourierdlem64  38072  fourierdlem79  38087  elaa2lem  38135  elaa2lemOLD  38136  etransclem16  38153  etransclem24  38161  etransclem31  38168  etransclem33  38170  etransclem34  38171  etransclem48OLD  38185  etransclem48  38186  rrxbasefi  38190  salgencl  38229  salexct  38231  salgenuni  38234  meadjiunlem  38341  caragenss  38363  caratheodory  38387  ovnlecvr  38418  ovnsslelem  38420  ovnlerp  38422  ovn0lem  38425  ovnsubaddlem1  38430  hoidmv1lelem1  38451  hoidmv1lelem3  38453  hoidmvlelem1  38455  hoidmvlelem2  38456  hoidmvlelem3  38457  hoidmvlelem4  38458  ovnhoilem1  38461  ovnhoilem2  38462  ovnlecvr2  38470  ovncvr2  38471  opnvonmbllem2  38493  perfectALTVlem2  38882  incistruhgr  39218  upgrss  39227  upgrn0  39228  upgruhgr  39238  usgrss  39309  uspgrushgr  39310  ushgredgedga  39356  ushgredgedgaloop  39358  vtxduhgrun  39588  rabsubmgmd  40064  mgmhmeql  40076  oddibas  40086  2zlidl  40207  2zrngbas  40209  2zrng0  40211
  Copyright terms: Public domain W3C validator