Theorem eleq2i 2693

Description: Inference from equality to equivalence of membership. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
eleq1i.1	|- A = B

Assertion

Ref	Expression
eleq2i	|- ( C e. A <-> C e. B )

Proof of Theorem eleq2i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 |- A = B
2		eleq2 2690	. 2 |- ( A = B -> ( C e. A <-> C e. B ) )
3	1, 2	ax-mp 5	1 |- ( C e. A <-> C e. B )

Syntax hints:   <-> wb 196   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  eleq12i  2694  eleqtri  2699  eleq2s  2719  hbxfreq  2730  raleqbii  2990  rexeqbii  3054  rabeq2i  3197  elab2g  3353  elrabf  3360  elrab3t  3362  elrab2  3366  cbvsbc  3464  elin2  3801  elsymdif  3849  dfnul2  3917  noel  3919  eltpg  4227  tpid3gOLD  4306  elunirab  4448  elintrab  4488  disjxiun  4649  disjxiunOLD  4650  exss  4931  elopOLD  4936  otiunsndisj  4980  brabsb  4986  brabga  4989  pofun  5051  elxp  5131  opeliunxp  5170  bropaex12  5192  brab2a  5194  elcnv  5299  elrnmptg  5375  opelres  5401  rninxp  5573  elsuci  5791  elsucg  5792  elsuc2g  5793  elfv  6189  0fv  6227  opabiota  6261  dffv2  6271  fvopab3g  6277  fvmptex  6294  fvopab5  6309  fvn0ssdmfun  6350  fveqressseq  6355  f0cli  6370  fmptco  6396  fvrnressn  6428  funfvima  6492  elunirnALT  6510  fliftel  6559  eloprabga  6747  elrnmpt2  6773  ovid  6777  offval  6904  suceloni  7013  1st2val  7194  2nd2val  7195  bropopvvv  7255  bropfvvvv  7257  fsplit  7282  xporderlem  7288  brtpos2  7358  wfrdmcl  7423  wfrfun  7425  wfrlem12  7426  wfrlem17  7431  wfr2  7434  issmo  7445  smores3  7450  tfrlem7  7479  tfrlem9  7481  tfrlem9a  7482  tfr2b  7492  tfr2  7494  rdgsuc  7520  frsucmptn  7534  tz7.48-2  7537  el1o  7579  dif1o  7580  ondif2  7582  oawordeulem  7634  elecg  7785  brecop  7840  erovlem  7843  eceqoveq  7853  mapsncnv  7904  mptelixpg  7945  brsdom  7978  isfi  7979  enssdom  7980  brdom2  7985  map1  8036  xpcomco  8050  brsdom2  8084  en3lplem2  8512  cnfcom2lem  8598  epfrs  8607  r1limg  8634  r1ord  8643  r1ord3  8645  tz9.12lem3  8652  rankvaln  8662  r1elss  8669  rankpwi  8686  ssrankr1  8698  r1val3  8701  r1pw  8708  rankr1b  8727  isnum2  8771  cardprclem  8805  infxpenlem  8836  alephcard  8893  alephnbtwn  8894  alephnbtwn2  8895  alephord2  8899  alephsdom  8909  dfac3  8944  dfac5lem2  8947  dfac5lem3  8948  dfac5lem5  8950  pwsdompw  9026  cfub  9071  cardcf  9074  cflecard  9075  cfle  9076  cflim2  9085  cofsmo  9091  cfidm  9097  isfin3  9118  isfin5  9121  isfin6  9122  sdom2en01  9124  fin23lem26  9147  fin23lem30  9164  isf32lem5  9179  itunitc1  9242  ituniiun  9244  axdc3lem3  9274  axcclem  9279  axdclem  9341  iunfo  9361  iundom2g  9362  cardidg  9370  konigthlem  9390  alephadd  9399  alephreg  9404  pwcfsdom  9405  cfpwsdom  9406  elgch  9444  fpwwe2lem12  9463  canth4  9469  wunex2  9560  r1tskina  9604  elni  9698  nlt1pi  9728  adderpq  9778  mulerpq  9779  recmulnq  9786  addsrpr  9896  mulsrpr  9897  opelcn  9950  opelreal  9951  elreal  9952  elreal2  9953  0ncn  9954  addcnsr  9956  mulcnsr  9957  xrlenlt  10103  elnn0  11294  elnnne0  11306  un0addcl  11326  un0mulcl  11327  elxnn0  11365  uztrn2  11705  elnnuz  11724  elnn0uz  11725  elq  11790  elxr  11950  elfzm1b  12418  elfz0lmr  12583  uzrdgfni  12757  fzennn  12767  fsuppmapnn0fiubOLD  12791  ser0  12853  hash2pwpr  13258  iswrd  13307  s3iunsndisj  13707  sumz  14453  sumss  14455  fsumcvg3  14460  abscvgcvg  14551  isumshft  14571  prodf1  14623  zprod  14667  prod1  14674  prodss  14677  prodsn  14692  prodsnf  14694  bpolydiflem  14785  bpoly2  14788  bpoly3  14789  bpoly4  14790  ruclem6  14964  divides  14985  dvdsflip  15039  pwp1fsum  15114  sadc0  15176  eulerthlem2  15487  prm23lt5  15519  4sqlem2  15653  4sqlem12  15660  vdwpc  15684  xpscf  16226  cidpropd  16370  oppcsect  16438  funcpropd  16560  natpropd  16636  initoeu2lem0  16663  arwhoma  16695  eldmcoa  16715  pospo  16973  psss  17214  ismgmn0  17244  gsumpropd2lem  17273  dfgrp2e  17448  ghmeqker  17687  cntri  17763  oppgsubg  17793  fvcosymgeq  17849  symgfixels  17854  pmtrfrn  17878  efgsfo  18152  efgrelexlemb  18163  lt6abl  18296  dmdprd  18397  dprdval  18402  dprdw  18409  srgbinomlem4  18543  isnirred  18700  isrhm  18721  issrng  18850  lspexchn2  19131  lspindp2l  19134  lspindp2  19135  lbsextlem2  19159  evlslem4  19508  ply1bascl2  19574  cply1mul  19664  lply1binom  19676  cnfldfunALT  19759  dsmmelbas  20083  frlmbas3  20115  lindsind2  20158  islindf4  20177  matsubgcell  20240  matinvgcell  20241  matvscacell  20242  matepmcl  20268  matepm2cl  20269  scmatscm  20319  smatvscl  20330  marrepcl  20370  marepvcl  20375  mulmarep1el  20378  mulmarep1gsum1  20379  mulmarep1gsum2  20380  submabas  20384  m1detdiag  20403  mdetdiag  20405  m2detleib  20437  gsummatr01lem3  20463  gsummatr01  20465  smadiadetlem4  20475  slesolinv  20486  slesolinvbi  20487  slesolex  20488  cramerimplem2  20490  pmatcoe1fsupp  20506  mat2pmatbas  20531  mat2pmatmul  20536  mat2pmatlin  20540  decpmatmul  20577  monmatcollpw  20584  pm2mpf1  20604  pm2mpghm  20621  istps  20738  mretopd  20896  neiptopuni  20934  lpdifsn  20947  restcls  20985  perfopn  20989  pnfnei  21024  mnfnei  21025  lmss  21102  hauscmplem  21209  is2ndc  21249  2ndcdisj  21259  hausnlly  21296  txuni2  21368  ptpjpre1  21374  elpt  21375  dfac14  21421  xkococn  21463  fbasrn  21688  fin1aufil  21736  elfm2  21752  elfm3  21754  fbflim  21780  flffbas  21799  cnpflf2  21804  fclsbas  21825  tsmssubm  21946  iscusp2  22106  imasdsf1olem  22178  metustel  22355  metuel2  22370  isnghm  22527  opnreen  22634  iccpnfcnv  22743  cvsi  22930  minveclem3b  23199  ovoliunlem1  23270  ioombl1lem4  23329  subopnmbl  23372  vitalilem2  23378  vitalilem3  23379  mbfimaopnlem  23422  mbfimaopn2  23424  itg2l  23496  dvply1  24039  vieta1lem1  24065  vieta1lem2  24066  elaa  24071  taylthlem2  24128  abelthlem6  24190  abelthlem9  24194  sinq34lt0t  24261  ellogrn  24306  dvrelog  24383  ellogdm  24385  logtayl2  24408  cxpcn3lem  24488  cxpcn3  24489  1cubr  24569  atandm  24603  atanf  24607  reasinsin  24623  atans2  24658  dmarea  24684  xrlimcnp  24695  amgmlem  24716  ppiublem1  24927  lgsdir2lem2  25051  gausslemma2dlem1a  25090  lgsquadlem1  25105  lgsquadlem2  25106  2sqlem1  25142  rpvmasum2  25201  eleenn  25776  edgiedgb  25947  isuhgr  25955  isushgr  25956  isupgr  25979  isumgr  25990  umgredg  26033  umgrpredgv  26035  umgredgne  26040  umgredgnlp  26042  isuspgr  26047  isusgr  26048  ausgrusgri  26063  usgredgppr  26088  edgssv2  26090  uspgredg2vlem  26115  uspgredg2v  26116  ushgredgedg  26121  ushgredgedgloop  26123  griedg0ssusgr  26157  uhgrissubgr  26167  subumgredg2  26177  uhgrspansubgrlem  26182  umgrres1lem  26202  upgrres1  26205  nbgrcl  26233  nbuhgr  26239  nbuhgr2vtx1edgblem  26247  nbupgrres  26266  edgnbusgreu  26269  nbusgredgeu0  26270  nbusgrf1o0  26271  hashnbusgrnn0  26278  nbupgruvtxres  26308  cffldtocusgr  26343  cusgrfilem2  26352  vtxdg0v  26369  vtxduhgr0nedg  26388  uhgrvd00  26430  vtxdginducedm1  26439  finsumvtxdg2ssteplem4  26444  rgrx0ndm  26489  wlk1walk  26535  wlkp1lem6  26575  iswwlks  26728  wspthnonp  26744  wwlksn0  26748  wlkiswwlksupgr2  26763  wlknwwlksnsur  26776  wwlksnwwlksnon  26810  2pthon3v  26839  umgr2wlk  26845  elwwlks2ons3  26848  elwwlks2s3  26859  rusgrnumwlkg  26872  isclwwlks  26880  clwlkclwwlk  26903  wwlksext2clwwlk  26924  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwlksfclwwlk  26962  1pthon2v  27013  uhgr3cyclex  27042  isconngr  27049  isconngr1  27050  eucrctshift  27103  isfrgr  27122  frgrnbnb  27157  frgrncvvdeqlem1  27163  frgrncvvdeqlem2  27164  frgrncvvdeqlem3  27165  frgrncvvdeqlem9  27171  fusgreghash2wspv  27199  numclwwlkovf2  27217  numclwwlk2lem1  27235  numclwlk2lem2f1o  27238  topnfbey  27325  isvclem  27432  isnvlem  27465  vsfval  27488  h2hlm  27837  hhcmpl  28057  hhcms  28060  elch0  28111  omlsilem  28261  h1de2ctlem  28414  elspansni  28417  nonbooli  28510  spansncvi  28511  adjeq  28794  cnlnssadj  28939  cnvbraval  28969  brabgaf  29420  elimampt  29438  fmptdF  29456  fmptcof2  29457  acunirnmpt  29459  acunirnmpt2  29460  ofpreima  29465  fcnvgreu  29472  1stpreima  29484  2ndpreima  29485  fz2ssnn0  29547  elxrge02  29640  psgnfzto1stlem  29850  submatres  29872  lmat22lem  29883  crefdf  29915  cmppcmp  29925  prsdm  29960  prsrn  29961  xrge0iifcnv  29979  xrge0iifiso  29981  xrge0iifhom  29983  pnfneige0  29997  qqhre  30064  rrhre  30065  esumnul  30110  esumcvgsum  30150  ldgenpisyslem1  30226  measvuni  30277  cntnevol  30291  dya2iocnrect  30343  sibf0  30396  oddpwdc  30416  eulerpartlemd  30428  eulerpartgbij  30434  eulerpartlemgh  30440  isrrvv  30505  coinfliprv  30544  ballotlem7  30597  signswch  30638  hashreprin  30698  chtvalz  30707  circlemethhgt  30721  hgt750lemb  30734  tgoldbachgt  30741  bnj23  30784  bnj158  30797  bnj168  30798  bnj1138  30859  bnj1143  30861  bnj1454  30912  bnj110  30928  bnj882  30996  bnj893  30998  bnj916  31003  bnj970  31017  bnj983  31021  bnj984  31022  bnj1137  31063  bnj1174  31071  bnj1388  31101  bnj1398  31102  subfacp1lem5  31166  mrsub0  31413  mrsubccat  31415  mrsubcn  31416  elmrsubrn  31417  msubco  31428  msubvrs  31457  elmthm  31473  mthmblem  31477  elrn3  31652  dfon2lem7  31694  eltrpred  31726  frrlem5e  31788  frrlem11  31792  madeval2  31936  brsset  31996  eltrans  31998  elfix  32010  ellimits  32017  elfuns  32022  elsingles  32025  fvtransport  32139  brcolinear2  32165  fvray  32248  linedegen  32250  fvline  32251  ellines  32259  fwddifn0  32271  elhf  32281  hfninf  32293  fnessref  32352  bj-csbsnlem  32898  bj-sels  32950  bj-eltag  32965  bj-sngltag  32971  bj-projun  32982  bj-0nelmpt  33069  bj-elid  33085  bj-elccinfty  33101  f1omptsnlem  33183  icoreelrnab  33202  relowlpssretop  33212  finxpnom  33238  uncov  33390  tan2h  33401  ptrecube  33409  poimirlem25  33434  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  cnambfre  33458  ftc1cnnc  33484  sdclem2  33538  sdclem1  33539  fdc  33541  caushft  33557  issmgrpOLD  33662  ismndo  33671  isrngo  33696  isdivrngo  33749  csbcom2fi  33934  elecALTV  34030  dath  35022  diclspsn  36483  dvh4dimlem  36732  dvh2dim  36734  dvh3dim3N  36738  lcfrvalsnN  36830  mapdh6eN  37029  mapdh7dN  37039  mapdh8b  37069  hdmap1l6e  37104  pellex  37399  rmspecnonsq  37472  islmodfg  37639  aaitgo  37732  areaquad  37802  elcnvcnvintab  37888  elnonrel  37891  elcnvcnvlem  37905  cnvcnvintabd  37906  brfvrcld2  37984  dvgrat  38511  cvgdvgrat  38512  radcnvrat  38513  nznngen  38515  uzmptshftfval  38545  binomcxplemcvg  38553  binomcxplemnotnn0  38555  tpid3gVD  39077  en3lplem2VD  39079  rexanuz3  39275  eliuniin  39279  eliuniin2  39303  disjinfi  39380  fsneq  39398  iuneqfzuzlem  39550  allbutfi  39616  eluzelz2  39627  uz0  39639  uzublem  39657  uzid3  39662  elicores  39760  uzinico  39787  climsuselem1  39839  climsuse  39840  islptre  39851  fnlimfvre  39906  limsupresico  39932  limsupvaluz  39940  limsupubuzlem  39944  limsupequzmptlem  39960  liminfresico  40003  cnrefiisplem  40055  stoweidlem14  40231  stoweidlem39  40256  stoweidlem48  40265  stoweidlem51  40268  stoweidlem59  40276  stoweidlem62  40279  wallispilem3  40284  fourierdlem42  40366  fourierdlem62  40385  fourierdlem80  40403  fourierdlem103  40426  fourierdlem104  40427  etransclem26  40477  rrxsnicc  40520  ioorrnopn  40525  ioorrnopnxr  40527  sge00  40593  sge0fodjrnlem  40633  sge0isum  40644  sge0seq  40663  ismea  40668  meadjiunlem  40682  carageneld  40716  volicorescl  40767  hoidmv1lelem1  40805  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem3  40811  ovnhoilem2  40816  hoiqssbllem2  40837  opnvonmbllem2  40847  ovolval4lem1  40863  iinhoiicc  40888  vonioolem1  40894  smflimlem1  40979  smflimlem2  40980  smflim  40985  nsssmfmbf  40987  smfresal  40995  smfrec  40996  smfdiv  41004  smfpimbor1lem2  41006  smflim2  41012  smflimmpt  41016  smfsupmpt  41021  smfinflem  41023  smfinfmpt  41025  smflimsuplem1  41026  smflimsuplem2  41027  smflimsuplem3  41028  smflimsuplem5  41030  smflimsuplem6  41031  smflimsup  41034  smflimsupmpt  41035  smfliminfmpt  41038  ndmaovcl  41283  ndmaovcom  41285  ndmaovass  41286  ndmaovdistr  41287  otiunsndisjX  41298  pfxccatpfx1  41427  fmtno4prmfac  41484  dfodd5  41572  sbgoldbo  41675  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  sprsymrelfolem2  41743  sprsymrelf  41745  sprsymrelf1  41746  uspgrsprf  41754  uspgrsprf1  41755  uspgrsprfo  41756  opeliun2xp  42111  ply1sclrmsm  42171  lcoop  42200  lincfsuppcl  42202  linccl  42203  lincvalsng  42205  lincvalpr  42207  lincvalsc0  42210  linc0scn0  42212  lincdifsn  42213  linc1  42214  lincsum  42218  lincscm  42219  lspsslco  42226  snlindsntor  42260  lincresunit3lem2  42269  ldepsnlinclem1  42294  ldepsnlinclem2  42295  elpglem3  42456