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

Theorem eleq2i 2881
Description: Inference from equality to equivalence of membership. (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
eleq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
eleq2i (𝐶𝐴𝐶𝐵)

Proof of Theorem eleq2i
StepHypRef Expression
1 eleq1i.1 . 2 𝐴 = 𝐵
2 eleq2 2878 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538  wcel 2111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870
This theorem is referenced by:  eleq12i  2882  eleqtri  2888  eleq2s  2908  hbxfreq  2919  nfceqi  2952  raleqbii  3197  rexeqbii  3285  rabeqi  3429  rabeq2i  3435  elab2gw  3613  elab2g  3616  elrabf  3624  elrab3t  3627  elrab2  3631  cbvsbcw  3752  cbvsbc  3754  elin2  4124  elsymdif  4174  noel  4247  eltpg  4583  elunirab  4816  elintrab  4850  disjxiun  5027  exss  5320  otiunsndisj  5375  brabsb  5383  brabga  5386  epelg  5431  pofun  5455  elxp  5542  opeliunxp  5583  bropaex12  5606  brab2a  5608  elcnv  5711  dmopabelb  5749  elrnmptg  5795  elres  5857  elrid  5880  rninxp  6003  elid  6023  elsuci  6225  elsucg  6226  elsuc2g  6227  elfv  6643  0fv  6684  opabiota  6721  dffv2  6733  fvopab3g  6740  fvmptex  6759  fvopab5  6777  fvn0ssdmfun  6819  fveqressseq  6824  f0cli  6841  fmptco  6868  fvrnressn  6900  funfvima  6970  elunirnALT  6989  fliftel  7041  eloprabga  7240  elrnmpo  7266  ovid  7270  offval  7396  suceloni  7508  1st2val  7699  2nd2val  7700  bropopvvv  7768  bropfvvvv  7770  fsplit  7795  fsplitOLD  7796  xporderlem  7804  brtpos2  7881  wfrdmcl  7946  wfrfun  7948  wfrlem12  7949  wfrlem17  7954  wfr2  7957  issmo  7968  smores3  7973  tfrlem7  8002  tfrlem9  8004  tfrlem9a  8005  tfr2b  8015  tfr2  8017  rdgsuc  8043  frsucmptn  8057  tz7.48-2  8061  el1o  8107  dif1o  8108  ondif2  8110  oawordeulem  8163  elecg  8315  brecop  8373  erovlem  8376  eceqoveq  8385  mapsncnv  8440  mptelixpg  8482  brsdom  8515  isfi  8516  enssdom  8517  brdom2  8522  xpcomco  8590  brsdom2  8625  en3lplem2  9060  cnfcom2lem  9148  epfrs  9157  r1limg  9184  r1ord  9193  r1ord3  9195  tz9.12lem3  9202  rankvaln  9212  r1elss  9219  rankpwi  9236  ssrankr1  9248  r1val3  9251  r1pw  9258  rankr1b  9277  djur  9332  djuunxp  9334  eldju2ndl  9337  eldju2ndr  9338  isnum2  9358  cardprclem  9392  infxpenlem  9424  alephcard  9481  alephnbtwn  9482  alephnbtwn2  9483  alephord2  9487  alephsdom  9497  dfac3  9532  dfac5lem2  9535  dfac5lem3  9536  dfac5lem5  9538  pwsdompw  9615  cfub  9660  cardcf  9663  cflecard  9664  cfle  9665  cflim2  9674  cofsmo  9680  cfidm  9686  isfin3  9707  isfin5  9710  isfin6  9711  sdom2en01  9713  fin23lem26  9736  fin23lem30  9753  isf32lem5  9768  itunitc1  9831  ituniiun  9833  axdc3lem3  9863  axcclem  9868  axdclem  9930  iunfo  9950  iundom2g  9951  cardidg  9959  konigthlem  9979  alephadd  9988  alephreg  9993  pwcfsdom  9994  cfpwsdom  9995  elgch  10033  fpwwe2lem12  10052  canth4  10058  wunex2  10149  r1tskina  10193  elni  10287  nlt1pi  10317  adderpq  10367  mulerpq  10368  recmulnq  10375  addsrpr  10486  mulsrpr  10487  opelcn  10540  opelreal  10541  elreal  10542  elreal2  10543  0ncn  10544  addcnsr  10546  mulcnsr  10547  xrlenlt  10695  elnn0  11887  elnnne0  11899  un0addcl  11918  un0mulcl  11919  elxnn0  11957  uztrn2  12250  elnnuz  12270  elnn0uz  12271  elq  12338  elxr  12499  elfzm1b  12980  elfz0lmr  13147  uzrdgfni  13321  fzennn  13331  ser0  13418  hash2pwpr  13830  iswrd  13859  pfxccatpfx1  14089  s3iunsndisj  14319  sumz  15071  sumss  15073  fsumcvg3  15078  abscvgcvg  15166  isumshft  15186  prodf1  15239  zprod  15283  prod1  15290  prodss  15293  prodsn  15308  prodsnf  15310  bpolydiflem  15400  bpoly2  15403  bpoly3  15404  bpoly4  15405  ruclem6  15580  divides  15601  dvdsflip  15659  pwp1fsum  15732  sadc0  15793  eulerthlem2  16109  prm23lt5  16141  4sqlem2  16275  4sqlem12  16282  vdwpc  16306  xpscf  16830  cidpropd  16972  oppcsect  17040  funcpropd  17162  natpropd  17238  initoeu2lem0  17265  arwhoma  17297  eldmcoa  17317  pospo  17575  psss  17816  ismgmn0  17846  gsumpropd2lem  17881  elefmndbas  18030  smndex1basss  18062  smndex1mgm  18064  pwmnd  18094  dfgrp2e  18121  mulgfval  18218  cycsubmel  18335  ghmeqker  18377  cntri  18453  oppgsubg  18483  fvcosymgeq  18549  symgfixels  18554  pmtrfrn  18578  efgsfo  18857  efgrelexlemb  18868  lt6abl  19008  dmdprd  19113  dprdval  19118  dprdw  19125  srgbinomlem4  19286  isnirred  19446  isrhm  19469  issrng  19614  lspexchn2  19896  lspindp2l  19899  lspindp2  19900  lbsextlem2  19924  cnfldfunALT  20104  dsmmelbas  20428  frlmbas3  20465  lindsind2  20508  islindf4  20527  evlslem4  20747  ply1bascl2  20833  cply1mul  20923  lply1binom  20935  matsubgcell  21039  matinvgcell  21040  matvscacell  21041  matepmcl  21067  matepm2cl  21068  scmatscm  21118  smatvscl  21129  marrepcl  21169  marepvcl  21174  mulmarep1el  21177  mulmarep1gsum1  21178  mulmarep1gsum2  21179  submabas  21183  m1detdiag  21202  mdetdiag  21204  m2detleib  21236  gsummatr01lem3  21262  gsummatr01  21264  smadiadetlem4  21274  slesolinv  21285  slesolinvbi  21286  slesolex  21287  cramerimplem2  21289  pmatcoe1fsupp  21306  mat2pmatbas  21331  mat2pmatmul  21336  mat2pmatlin  21340  decpmatmul  21377  monmatcollpw  21384  pm2mpf1  21404  pm2mpghm  21421  istps  21539  mretopd  21697  neiptopuni  21735  lpdifsn  21748  restcls  21786  perfopn  21790  pnfnei  21825  mnfnei  21826  lmss  21903  hauscmplem  22011  is2ndc  22051  2ndcdisj  22061  hausnlly  22098  txuni2  22170  ptpjpre1  22176  elpt  22177  dfac14  22223  xkococn  22265  fbasrn  22489  fin1aufil  22537  elfm2  22553  elfm3  22555  fbflim  22581  flffbas  22600  cnpflf2  22605  fclsbas  22626  efmndtmd  22706  tsmssubm  22748  iscusp2  22908  imasdsf1olem  22980  metustel  23157  metuel2  23172  isnghm  23329  opnreen  23436  iccpnfcnv  23549  ehleudisval  24023  ehl1eudis  24024  ehl2eudis  24026  minveclem3b  24032  ovoliunlem1  24106  ioombl1lem4  24165  subopnmbl  24208  vitalilem2  24213  vitalilem3  24214  mbfimaopnlem  24259  mbfimaopn2  24261  itg2l  24333  dvply1  24880  vieta1lem1  24906  vieta1lem2  24907  elaa  24912  taylthlem2  24969  abelthlem6  25031  abelthlem9  25035  sinq34lt0t  25102  ellogrn  25151  dvrelog  25228  ellogdm  25230  logtayl2  25253  cxpcn3lem  25336  cxpcn3  25337  1cubr  25428  atandm  25462  atanf  25466  reasinsin  25482  atans2  25517  dmarea  25543  xrlimcnp  25554  amgmlem  25575  ppiublem1  25786  lgsdir2lem2  25910  gausslemma2dlem1a  25949  lgsquadlem1  25964  lgsquadlem2  25965  2sqlem1  26001  rpvmasum2  26096  edgiedgb  26847  isuhgr  26853  isushgr  26854  isupgr  26877  isumgr  26888  umgredg  26931  umgrpredgv  26933  umgredgne  26938  umgredgnlp  26940  isuspgr  26945  isusgr  26946  ausgrusgri  26961  usgredgppr  26986  edgssv2  26988  uspgredg2vlem  27013  uspgredg2v  27014  ushgredgedg  27019  ushgredgedgloop  27021  griedg0ssusgr  27055  uhgrissubgr  27065  subumgredg2  27075  uhgrspansubgrlem  27080  umgrres1lem  27100  upgrres1  27103  nbgrcl  27125  nbuhgr  27133  nbuhgr2vtx1edgblem  27141  nbupgrres  27154  edgnbusgreu  27157  nbusgredgeu0  27158  nbusgrf1o0  27159  hashnbusgrnn0  27166  nbupgruvtxres  27197  cffldtocusgr  27237  cusgrfilem2  27246  vtxdg0v  27263  vtxduhgr0nedg  27282  uhgrvd00  27324  vtxdginducedm1  27333  finsumvtxdg2ssteplem4  27338  wlk1walk  27428  wlkp1lem6  27468  iswwlks  27622  wwlknllvtx  27632  wwlksonvtx  27641  wspthnonp  27645  wlkiswwlksupgr2  27663  wwlksnwwlksnon  27701  2pthon3v  27729  umgr2wlk  27735  elwwlks2s3  27737  wwlks2onv  27739  elwwlks2ons3im  27740  isclwwlk  27769  clwwlkccatlem  27774  clwlkclwwlk  27787  wwlksext2clwwlk  27842  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  clwwlknon1  27882  clwwlknon1nloop  27884  clwwlknon2x  27888  1pthon2v  27938  uhgr3cyclex  27967  isconngr  27974  isconngr1  27975  eucrctshift  28028  frgrnbnb  28078  frgrncvvdeqlem1  28084  frgrncvvdeqlem2  28085  frgrncvvdeqlem3  28086  frgrncvvdeqlem9  28092  fusgreghash2wspv  28120  extwwlkfab  28137  numclwwlk1lem2foa  28139  numclwwlk1lem2fo  28143  clwlknon2num  28153  numclwlk2lem2f1o  28164  numclwwlk5lem  28172  topnfbey  28254  isvclem  28360  isnvlem  28393  vsfval  28416  h2hlm  28763  hhcmpl  28983  hhcms  28986  elch0  29037  omlsilem  29185  h1de2ctlem  29338  elspansni  29341  nonbooli  29434  spansncvi  29435  adjeq  29718  cnlnssadj  29863  cnvbraval  29893  brabgaf  30372  elimampt  30397  2ndresdju  30411  fmptdF  30419  fmptcof2  30420  acunirnmpt  30422  acunirnmpt2  30423  ofpreima  30428  fcnvgreu  30436  fdifsuppconst  30449  1stpreima  30466  2ndpreima  30467  fz2ssnn0  30534  elxrge02  30634  psgnfzto1stlem  30792  cycpmgcl  30845  prmidl0  31034  submatres  31159  lmat22lem  31170  crefdf  31201  cmppcmp  31211  rspectopn  31220  prsdm  31267  prsrn  31268  xrge0iifcnv  31286  xrge0iifiso  31288  xrge0iifhom  31290  pnfneige0  31304  qqhre  31371  rrhre  31372  esumnul  31417  esumcvgsum  31457  ldgenpisyslem1  31532  measvuni  31583  cntnevol  31597  dya2iocnrect  31649  sibf0  31702  oddpwdc  31722  eulerpartlemd  31734  eulerpartgbij  31740  eulerpartlemgh  31746  isrrvv  31811  coinfliprv  31850  ballotlem7  31903  signswch  31941  hashreprin  32001  chtvalz  32010  circlemethhgt  32024  hgt750lemb  32037  tgoldbachgt  32044  bnj23  32098  bnj158  32109  bnj168  32110  bnj1138  32170  bnj1143  32172  bnj1454  32224  bnj110  32240  bnj882  32308  bnj893  32310  bnj916  32315  bnj970  32329  bnj983  32333  bnj984  32334  bnj1137  32377  bnj1174  32385  bnj1388  32415  bnj1398  32416  loop1cycl  32494  subfacp1lem5  32541  satfv1  32720  satfrnmapom  32727  satf0op  32734  satf0n0  32735  fmlafvel  32742  fmlaomn0  32747  fmlan0  32748  satffunlem2lem2  32763  satfv0fvfmla0  32770  satefvfmla0  32775  mrsub0  32873  mrsubccat  32875  mrsubcn  32876  elmrsubrn  32877  msubco  32888  msubvrs  32917  elmthm  32933  mthmblem  32937  elrn3  33108  dfon2lem7  33144  eltrpred  33175  frrlem8  33240  frrlem9  33241  frrlem10  33242  madeval2  33400  brsset  33460  eltrans  33462  elfix  33474  ellimits  33481  elfuns  33486  elsingles  33489  fvtransport  33603  brcolinear2  33629  fvray  33712  linedegen  33714  fvline  33715  ellines  33723  fwddifn0  33735  elhf  33745  hfninf  33757  fnessref  33815  bj-ififc  34025  bj-csbsnlem  34341  currysetlem1  34379  bj-eltag  34410  bj-sngltag  34416  bj-projun  34427  bj-0nelmpt  34528  bj-opelidres  34573  bj-inftyexpitaudisj  34617  bj-elccinfty  34626  f1omptsnlem  34750  icoreelrnab  34768  relowlpssretop  34778  rdgssun  34792  exrecfnlem  34793  finxpnom  34815  uncov  35035  tan2h  35046  ptrecube  35054  poimirlem25  35079  poimirlem29  35083  poimirlem30  35084  poimirlem31  35085  poimirlem32  35086  cnambfre  35102  ftc1cnnc  35126  sdclem2  35177  sdclem1  35178  fdc  35180  caushft  35196  issmgrpOLD  35298  ismndo  35307  isrngo  35332  isdivrngo  35385  csbcom2fi  35563  elecALTV  35684  brrabga  35755  eldmcoss  35855  coss0  35876  elrels2  35883  dath  37029  diclspsn  38487  dvh4dimlem  38736  dvh2dim  38738  dvh3dim3N  38742  lcfrvalsnN  38834  mapdh6eN  39033  mapdh7dN  39043  mapdh8b  39073  hdmap1l6e  39107  lcmfunnnd  39297  3factsumint1  39306  frlmfielbas  39429  pellex  39771  rmspecnonsq  39843  islmodfg  40008  aaitgo  40101  areaquad  40161  elcnvcnvintab  40277  elnonrel  40280  elcnvcnvlem  40294  cnvcnvintabd  40295  brfvrcld2  40388  grur1cld  40935  dvgrat  41011  cvgdvgrat  41012  radcnvrat  41013  nznngen  41015  uzmptshftfval  41045  binomcxplemcvg  41053  binomcxplemnotnn0  41055  tpid3gVD  41543  en3lplem2VD  41545  rexanuz3  41727  eliuniin  41730  eliuniin2  41750  disjinfi  41815  fsneq  41830  iuneqfzuzlem  41961  allbutfi  42024  eluzelz2  42035  uz0  42044  uzublem  42062  uzid3  42067  elicores  42165  uzinico  42192  climsuselem1  42244  climsuse  42245  islptre  42256  fnlimfvre  42311  limsupresico  42337  limsupvaluz  42345  limsupubuzlem  42349  limsupequzmptlem  42365  liminfresico  42408  cnrefiisplem  42466  stoweidlem14  42651  stoweidlem39  42676  stoweidlem48  42685  stoweidlem51  42688  stoweidlem59  42696  stoweidlem62  42699  wallispilem3  42704  fourierdlem42  42786  fourierdlem62  42805  fourierdlem80  42823  fourierdlem103  42846  fourierdlem104  42847  etransclem26  42897  rrxsnicc  42937  ioorrnopn  42942  ioorrnopnxr  42944  sge00  43010  sge0fodjrnlem  43050  sge0isum  43061  sge0seq  43080  meadjiunlem  43099  carageneld  43136  volicorescl  43187  hoidmv1lelem1  43225  hoidmv1le  43228  hoidmvlelem1  43229  hoidmvlelem3  43231  ovnhoilem2  43236  hoiqssbllem2  43257  opnvonmbllem2  43267  ovolval4lem1  43283  iinhoiicc  43308  vonioolem1  43314  smflimlem1  43399  smflimlem2  43400  smflim  43405  nsssmfmbf  43407  smfresal  43415  smfrec  43416  smfdiv  43424  smfpimbor1lem2  43426  smflim2  43432  smflimmpt  43436  smfsupmpt  43441  smfinflem  43443  smfinfmpt  43445  smflimsuplem1  43446  smflimsuplem2  43447  smflimsuplem3  43448  smflimsuplem5  43450  smflimsuplem6  43451  smflimsup  43454  smflimsupmpt  43455  smfliminfmpt  43458  ndmaovcl  43754  ndmaovcom  43756  ndmaovass  43757  ndmaovdistr  43758  dfatco  43807  otiunsndisjX  43830  fvmptrabdm  43844  elsetpreimafvb  43896  sprsymrelfolem2  44005  sprsymrelf  44007  sprsymrelf1  44008  prpair  44013  prproropf1olem0  44014  paireqne  44023  fmtno4prmfac  44084  dfodd5  44173  sbgoldbo  44300  nnsum4primeseven  44313  nnsum4primesevenALTV  44314  isomushgr  44339  isomuspgrlem2c  44343  uspgrsprf  44369  uspgrsprf1  44370  uspgrsprfo  44371  opeliun2xp  44729  ply1sclrmsm  44786  lcoop  44815  lincfsuppcl  44817  linccl  44818  lincvalsng  44820  lincvalpr  44822  lincvalsc0  44825  linc0scn0  44827  lincdifsn  44828  linc1  44829  lincsum  44833  lincscm  44834  lspsslco  44841  snlindsntor  44875  lincresunit3lem2  44884  ldepsnlinclem1  44909  ldepsnlinclem2  44910  prelrrx2  45122  prelrrx2b  45123  rrx2xpref1o  45127  rrx2plord  45129  rrx2linesl  45152  elpglem3  45237
  Copyright terms: Public domain W3C validator