Theorem eleq2i 2830

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

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eleq2 2827	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  eleq12i  2831  eleqtri  2836  eleq2s  2856  hbxfreq  2869  nfceqi  2899  raleqbii  3341  rexeqbii  3342  rabeqi  3446  rabrabi  3452  reqabi  3456  elab2gw  3679  elab2g  3682  elrabf  3690  elrab3t  3693  elrab2  3697  cbvsbcw  3824  cbvsbcvw  3825  cbvsbc  3826  elin2  4212  elsymdif  4263  noel  4343  eltpg  4690  elunirab  4926  elintrab  4964  disjxiun  5144  exss  5473  otiunsndisj  5529  brabsb  5540  brabga  5543  epelg  5589  pofun  5614  elxp  5711  opeliunxp  5755  bropaex12  5779  brab2a  5781  elcnv  5889  dmopabelb  5929  elrnmptg  5974  elres  6039  elimampt  6062  elrid  6065  rninxp  6200  elid  6220  elsuci  6452  elsucg  6453  elsuc2g  6454  elfv  6904  0fv  6950  opabiota  6990  dffv2  7003  fvopab3g  7010  fvmptex  7029  fvopab5  7048  fvn0ssdmfun  7093  fveqressseq  7098  f0cli  7117  fmptco  7148  fvrnressn  7180  funfvima  7249  elunirnALT  7271  fliftel  7328  eloprabga  7540  eloprabgaOLD  7541  elrnmpo  7568  elimampo  7569  ovid  7573  offval  7705  sucexeloniOLD  7829  suceloniOLD  7831  1st2val  8040  2nd2val  8041  bropopvvv  8113  bropfvvvv  8115  fsplit  8140  xporderlem  8150  frpoins3xpg  8163  frpoins3xp3g  8164  brtpos2  8255  frrlem8  8316  frrlem9  8317  frrlem10  8318  fprresex  8333  wfrdmclOLD  8355  wfrfunOLD  8357  wfrlem12OLD  8358  wfrlem17OLD  8363  wfr2OLD  8366  issmo  8386  smores3  8391  tfrlem7  8421  tfrlem9  8423  tfrlem9a  8424  tfr2b  8434  tfr2  8436  rdgsuc  8462  frsucmptn  8477  tz7.48-2  8480  el1o  8531  ord2eln012  8533  dif1o  8536  ondif2  8538  oawordeulem  8590  elecg  8787  brecop  8848  erovlem  8851  eceqoveq  8860  mapsncnv  8931  mptelixpg  8973  brsdom  9013  isfi  9014  enssdom  9015  brdom2  9020  xpcomco  9100  brsdom2  9135  en3lplem2  9650  cnfcom2lem  9738  brttrcl2  9751  ttrcltr  9753  rnttrcl  9759  epfrs  9768  r1limg  9808  r1ord  9817  r1ord3  9819  tz9.12lem3  9826  rankvaln  9836  r1elss  9843  rankpwi  9860  ssrankr1  9872  r1val3  9875  r1pw  9882  rankr1b  9901  djur  9956  djuunxp  9958  eldju2ndl  9961  eldju2ndr  9962  isnum2  9982  cardprclem  10016  infxpenlem  10050  alephcard  10107  alephnbtwn  10108  alephnbtwn2  10109  alephord2  10113  alephsdom  10123  dfac3  10158  dfac5lem2  10161  dfac5lem3  10162  dfac5lem5  10164  pwsdompw  10240  cfub  10286  cardcf  10289  cflecard  10290  cfle  10291  cflim2  10300  cofsmo  10306  cfidm  10312  isfin3  10333  isfin5  10336  isfin6  10337  sdom2en01  10339  fin23lem26  10362  fin23lem30  10379  isf32lem5  10394  itunitc1  10457  ituniiun  10459  axdc3lem3  10489  axcclem  10494  axdclem  10556  iunfo  10576  iundom2g  10577  cardidg  10585  konigthlem  10605  alephadd  10614  alephreg  10619  pwcfsdom  10620  cfpwsdom  10621  elgch  10659  fpwwe2lem11  10678  canth4  10684  wunex2  10775  r1tskina  10819  elni  10913  nlt1pi  10943  adderpq  10993  mulerpq  10994  recmulnq  11001  addsrpr  11112  mulsrpr  11113  opelcn  11166  opelreal  11167  elreal  11168  elreal2  11169  0ncn  11170  addcnsr  11172  mulcnsr  11173  xrlenlt  11323  elnn0  12525  elnnne0  12537  un0addcl  12556  un0mulcl  12557  elxnn0  12598  uztrn2  12894  elnnuz  12919  elnn0uz  12920  elq  12989  elxr  13155  elfzm1b  13638  elfz0lmr  13817  uzrdgfni  13995  fzennn  14005  ser0  14091  hash2pwpr  14511  iswrd  14550  pfxccatpfx1  14770  s3iunsndisj  15003  sumz  15754  sumss  15756  fsumcvg3  15761  abscvgcvg  15851  isumshft  15871  prodf1  15923  prodeq1i  15948  zprod  15969  prod1  15976  prodss  15979  prodsn  15994  prodsnf  15996  bpolydiflem  16086  bpoly2  16089  bpoly3  16090  bpoly4  16091  ruclem6  16267  divides  16288  dvdsflip  16350  pwp1fsum  16424  sadc0  16487  eulerthlem2  16815  prm23lt5  16847  4sqlem2  16982  4sqlem12  16989  vdwpc  17013  xpscf  17611  cidpropd  17754  oppcsect  17825  funcpropd  17953  natpropd  18032  dfinito2  18056  dftermo2  18057  initoeu2lem0  18066  arwhoma  18098  eldmcoa  18118  pospo  18402  psss  18637  ismgmn0  18667  gsumpropd2lem  18704  elefmndbas  18898  smndex1basss  18930  smndex1mgm  18932  pwmnd  18962  dfgrp2e  18993  mulgfval  19099  eqg0subg  19226  cycsubmel  19230  ghmeqker  19273  elcntr  19360  cntri  19362  cntzsgrpcl  19364  oppgsubg  19396  fvcosymgeq  19461  symgfixels  19466  pmtrfrn  19490  efgsfo  19771  efgrelexlemb  19782  lt6abl  19927  dmdprd  20032  dprdval  20037  dprdw  20044  srgbinomlem4  20246  isnirred  20436  isrhm  20494  issrng  20861  lspexchn2  21150  lspindp2l  21153  lspindp2  21154  lbsextlem2  21178  rnglidl1  21259  df2idl2  21284  2idlss  21289  rngqiprngimfo  21328  cnfldfun  21395  cnfldfunOLD  21408  pzriprnglem3  21511  pzriprnglem4  21512  pzriprnglem7  21515  pzriprnglem8  21516  pzriprnglem9  21517  pzriprnglem12  21520  pzriprnglem14  21522  dsmmelbas  21776  frlmbas3  21813  lindsind2  21856  islindf4  21875  psrbagf  21955  evlslem4  22117  psdmul  22187  ply1bascl2  22221  cply1mul  22315  lply1binom  22329  matsubgcell  22455  matinvgcell  22456  matvscacell  22457  matepmcl  22483  matepm2cl  22484  scmatscm  22534  smatvscl  22545  marrepcl  22585  marepvcl  22590  mulmarep1el  22593  mulmarep1gsum1  22594  mulmarep1gsum2  22595  submabas  22599  m1detdiag  22618  mdetdiag  22620  m2detleib  22652  gsummatr01lem3  22678  gsummatr01  22680  smadiadetlem4  22690  slesolinv  22701  slesolinvbi  22702  slesolex  22703  cramerimplem2  22705  pmatcoe1fsupp  22722  mat2pmatbas  22747  mat2pmatmul  22752  mat2pmatlin  22756  decpmatmul  22793  monmatcollpw  22800  pm2mpf1  22820  pm2mpghm  22837  istps  22955  mretopd  23115  neiptopuni  23153  lpdifsn  23166  restcls  23204  perfopn  23208  pnfnei  23243  mnfnei  23244  lmss  23321  hauscmplem  23429  is2ndc  23469  2ndcdisj  23479  hausnlly  23516  txuni2  23588  ptpjpre1  23594  elpt  23595  dfac14  23641  xkococn  23683  fbasrn  23907  fin1aufil  23955  elfm2  23971  elfm3  23973  fbflim  23999  flffbas  24018  cnpflf2  24023  fclsbas  24044  efmndtmd  24124  tsmssubm  24166  iscusp2  24326  imasdsf1olem  24398  metustel  24578  metuel2  24593  isnghm  24759  opnreen  24866  iccpnfcnv  24988  ehleudisval  25466  ehl1eudis  25467  ehl2eudis  25469  minveclem3b  25475  ovoliunlem1  25550  ioombl1lem4  25609  subopnmbl  25652  vitalilem2  25657  vitalilem3  25658  mbfimaopnlem  25703  mbfimaopn2  25705  itg2l  25778  dvply1  26339  vieta1lem1  26366  vieta1lem2  26367  elaa  26372  taylthlem2  26430  taylthlem2OLD  26431  abelthlem6  26494  abelthlem9  26498  sinq34lt0t  26565  ellogrn  26615  dvrelog  26693  ellogdm  26695  logtayl2  26718  cxpcn3lem  26804  cxpcn3  26805  1cubr  26899  atandm  26933  atanf  26937  reasinsin  26953  atans2  26988  dmarea  27014  xrlimcnp  27025  amgmlem  27047  ppiublem1  27260  lgsdir2lem2  27384  gausslemma2dlem1a  27423  lgsquadlem1  27438  lgsquadlem2  27439  2sqlem1  27475  rpvmasum2  27570  madeval2  27906  newval  27908  leftval  27916  rightval  27917  lltropt  27925  madess  27929  oldssmade  27930  lrold  27949  addsproplem2  28017  addsproplem4  28019  addsproplem6  28021  negsproplem4  28077  negsproplem6  28079  precsexlem10  28254  precsexlem11  28255  sltonold  28297  elnns  28357  elzs  28384  edgiedgb  29085  isuhgr  29091  isushgr  29092  isupgr  29115  isumgr  29126  umgredg  29169  umgrpredgv  29171  umgredgne  29176  umgredgnlp  29178  isuspgr  29183  isusgr  29184  ausgrusgri  29199  usgredgppr  29227  edgssv2  29229  uspgredg2vlem  29254  uspgredg2v  29255  ushgredgedg  29260  ushgredgedgloop  29262  griedg0ssusgr  29296  uhgrissubgr  29306  subumgredg2  29316  uhgrspansubgrlem  29321  umgrres1lem  29341  upgrres1  29344  nbgrcl  29366  nbuhgr  29374  nbuhgr2vtx1edgblem  29382  nbupgrres  29395  edgnbusgreu  29398  nbusgredgeu0  29399  nbusgrf1o0  29400  hashnbusgrnn0  29407  nbupgruvtxres  29438  cffldtocusgr  29478  cffldtocusgrOLD  29479  cusgrfilem2  29488  vtxdg0v  29505  vtxduhgr0nedg  29524  uhgrvd00  29566  vtxdginducedm1  29575  finsumvtxdg2ssteplem4  29580  wlk1walk  29671  wlkp1lem6  29710  iswwlks  29865  wwlknllvtx  29875  wwlksonvtx  29884  wspthnonp  29888  wlkiswwlksupgr2  29906  wwlksnwwlksnon  29944  2pthon3v  29972  umgr2wlk  29978  elwwlks2s3  29980  wwlks2onv  29982  elwwlks2ons3im  29983  isclwwlk  30012  clwwlkccatlem  30017  clwlkclwwlk  30030  wwlksext2clwwlk  30085  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  clwwlknon1  30125  clwwlknon1nloop  30127  clwwlknon2x  30131  1pthon2v  30181  uhgr3cyclex  30210  isconngr  30217  isconngr1  30218  eucrctshift  30271  frgrnbnb  30321  frgrncvvdeqlem1  30327  frgrncvvdeqlem2  30328  frgrncvvdeqlem3  30329  frgrncvvdeqlem9  30335  fusgreghash2wspv  30363  extwwlkfab  30380  numclwwlk1lem2foa  30382  numclwwlk1lem2fo  30386  clwlknon2num  30396  numclwlk2lem2f1o  30407  numclwwlk5lem  30415  topnfbey  30497  isvclem  30605  isnvlem  30638  vsfval  30661  h2hlm  31008  hhcmpl  31228  hhcms  31231  elch0  31282  omlsilem  31430  h1de2ctlem  31583  elspansni  31586  nonbooli  31679  spansncvi  31680  adjeq  31963  cnlnssadj  32108  cnvbraval  32138  brabgaf  32627  2ndresdju  32665  fmptdF  32672  fmptcof2  32673  acunirnmpt  32675  acunirnmpt2  32676  ofpreima  32681  fcnvgreu  32689  fdifsuppconst  32703  1stpreima  32721  2ndpreima  32722  fz2ssnn0  32793  elxrge02  32898  ccatws1f1o  32920  gsumwrd2dccatlem  33051  psgnfzto1stlem  33102  cycpmgcl  33155  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem4  33234  nsgqusf1olem2  33421  nsgqusf1olem3  33422  prmidl0  33457  crngmxidl  33476  opprnsg  33491  rprmirredb  33539  zringfrac  33561  evl1deg2  33581  evl1deg3  33582  ply1degltel  33594  ply1degleel  33595  constrsuc  33742  constrconj  33749  submatres  33766  lmat22lem  33777  crefdf  33808  cmppcmp  33818  rspectopn  33827  prsdm  33874  prsrn  33875  xrge0iifcnv  33893  xrge0iifiso  33895  xrge0iifhom  33897  pnfneige0  33911  qqhre  33982  rrhre  33983  esumnul  34028  esumcvgsum  34068  ldgenpisyslem1  34143  measvuni  34194  cntnevol  34208  dya2iocnrect  34262  sibf0  34315  oddpwdc  34335  eulerpartlemd  34347  eulerpartgbij  34353  eulerpartlemgh  34359  isrrvv  34424  coinfliprv  34463  ballotlem7  34516  signswch  34554  hashreprin  34613  chtvalz  34622  circlemethhgt  34636  hgt750lemb  34649  tgoldbachgt  34656  bnj23  34710  bnj158  34721  bnj168  34722  bnj1138  34780  bnj1143  34782  bnj1454  34834  bnj110  34850  bnj882  34918  bnj893  34920  bnj916  34925  bnj970  34939  bnj983  34943  bnj984  34944  bnj1137  34987  bnj1174  34995  bnj1388  35025  bnj1398  35026  loop1cycl  35121  subfacp1lem5  35168  satfv1  35347  satfrnmapom  35354  satf0op  35361  satf0n0  35362  fmlafvel  35369  fmlaomn0  35374  fmlan0  35375  satffunlem2lem2  35390  satfv0fvfmla0  35397  satefvfmla0  35402  mrsub0  35500  mrsubccat  35502  mrsubcn  35503  elmrsubrn  35504  msubco  35515  msubvrs  35544  elmthm  35560  mthmblem  35564  ellcsrspsn  35625  elrn3  35741  dfon2lem7  35770  brsset  35870  eltrans  35872  elfix  35884  ellimits  35891  elfuns  35896  elsingles  35899  fvtransport  36013  brcolinear2  36039  fvray  36122  linedegen  36124  fvline  36125  ellines  36133  fwddifn0  36145  elhf  36155  hfninf  36167  rmoeqi  36168  rmoeqbii  36169  reueqi  36170  reueqbii  36171  rabeqbii  36175  iuneq12i  36176  iineq1i  36177  iineq12i  36178  riotaeqbii  36179  ixpeq1i  36181  itgeq12i  36187  cbvprodvw2  36229  fnessref  36339  bj-ififc  36564  bj-csbsnlem  36885  bj-elgab  36921  currysetlem1  36929  bj-eltag  36959  bj-sngltag  36965  bj-projun  36976  bj-velpwALT  37035  bj-0nelmpt  37098  bj-opelidres  37143  bj-inftyexpitaudisj  37187  bj-elccinfty  37196  f1omptsnlem  37318  icoreelrnab  37336  relowlpssretop  37346  rdgssun  37360  exrecfnlem  37361  finxpnom  37383  uncov  37587  tan2h  37598  ptrecube  37606  poimirlem25  37631  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  cnambfre  37654  ftc1cnnc  37678  sdclem2  37728  sdclem1  37729  fdc  37731  caushft  37747  issmgrpOLD  37849  ismndo  37858  isrngo  37883  isdivrngo  37936  csbcom2fi  38114  elecALTV  38247  brrabga  38322  eldmcoss  38439  coss0  38460  elrels2  38467  dath  39718  diclspsn  41176  dvh4dimlem  41425  dvh2dim  41427  dvh3dim3N  41431  lcfrvalsnN  41523  mapdh6eN  41722  mapdh7dN  41732  mapdh8b  41762  hdmap1l6e  41796  lcmfunnnd  41993  3factsumint1  42002  primrootsunit1  42078  primrootscoprmpow  42080  aks6d1c2lem4  42108  sticksstones2  42128  sticksstones3  42129  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem2  42152  aks6d1c6lem3  42153  redvmptabs  42368  readvrec2  42369  readvrec  42370  frlmfielbas  42486  mhpind  42580  pellex  42822  rmspecnonsq  42894  islmodfg  43057  aaitgo  43150  areaquad  43204  ordeldif1o  43249  naddwordnexlem4  43390  fpwfvss  43401  finona1cl  43442  elcnvcnvintab  43571  elnonrel  43574  elcnvcnvlem  43588  cnvcnvintabd  43589  brfvrcld2  43681  grur1cld  44227  dvgrat  44307  cvgdvgrat  44308  radcnvrat  44309  nznngen  44311  uzmptshftfval  44341  binomcxplemcvg  44349  binomcxplemnotnn0  44351  tpid3gVD  44839  en3lplem2VD  44841  wfaxrep  44949  wfaxsep  44950  wfaxpr  44951  iuneq1i  45024  rexanuz3  45035  eliuniin  45038  eliuniin2  45059  disjinfi  45134  fsneq  45148  iuneqfzuzlem  45283  allbutfi  45342  eluzelz2  45352  uz0  45361  uzublem  45379  uzid3  45384  elicores  45485  uzinico  45512  climsuselem1  45562  climsuse  45563  islptre  45574  fnlimfvre  45629  limsupresico  45655  limsupvaluz  45663  limsupubuzlem  45667  limsupequzmptlem  45683  liminfresico  45726  cnrefiisplem  45784  stoweidlem14  45969  stoweidlem39  45994  stoweidlem48  46003  stoweidlem51  46006  stoweidlem59  46014  stoweidlem62  46017  wallispilem3  46022  fourierdlem42  46104  fourierdlem62  46123  fourierdlem80  46141  fourierdlem103  46164  fourierdlem104  46165  etransclem26  46215  rrxsnicc  46255  ioorrnopn  46260  ioorrnopnxr  46262  sge00  46331  sge0fodjrnlem  46371  sge0isum  46382  sge0seq  46401  meadjiunlem  46420  carageneld  46457  volicorescl  46508  hoidmv1lelem1  46546  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem3  46552  ovnhoilem2  46557  hoiqssbllem2  46578  opnvonmbllem2  46588  ovolval4lem1  46604  iinhoiicc  46629  vonioolem1  46635  smflimlem1  46726  smflimlem2  46727  smflim  46732  nsssmfmbf  46734  smfresal  46743  smfrec  46744  smfdiv  46752  smfpimbor1lem2  46754  smflim2  46761  smflimmpt  46765  smfinflem  46772  smflimsuplem1  46775  smflimsuplem2  46776  smflimsuplem3  46777  smflimsuplem5  46779  smflimsuplem6  46780  smflimsup  46783  smflimsupmpt  46784  smfliminfmpt  46787  fcores  47016  ndmaovcl  47152  ndmaovcom  47154  ndmaovass  47155  ndmaovdistr  47156  dfatco  47205  otiunsndisjX  47228  fvmptrabdm  47242  elsetpreimafvb  47308  sprsymrelfolem2  47417  sprsymrelf  47419  sprsymrelf1  47420  prpair  47425  prproropf1olem0  47426  paireqne  47435  fmtno4prmfac  47496  dfodd5  47584  sbgoldbo  47711  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  clnbgrcl  47745  clnbgredg  47763  sclnbgrel  47770  isubgredg  47789  isuspgrim0  47809  isuspgrimlem  47811  gricushgr  47823  clnbgrgrimlem  47838  grimedg  47840  usgrgrtrirex  47852  stgrnbgr0  47866  isubgr3stgrlem3  47870  isubgr3stgrlem4  47871  isubgr3stgrlem6  47873  isubgr3stgrlem7  47874  uspgrlimlem2  47891  uspgrlimlem3  47892  grlimgrtrilem1  47896  grlimgrtrilem2  47897  usgrexmpl2trifr  47931  gpgvtxel  47940  gpgedgel  47942  gpgusgralem  47945  gpg5order  47948  ceilhalfelfzo1  47950  gpgvtxedg0  47955  gpgvtxedg1  47956  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965  gpg3nbgrvtx1  47968  gpg5nbgrvtx03star  47970  gpg5nbgr3star  47971  gpgvtxdg3  47972  gpg5gricstgr3  47973  uspgrsprf  47989  uspgrsprf1  47990  uspgrsprfo  47991  opeliun2xp  48177  ply1sclrmsm  48228  lcoop  48256  lincfsuppcl  48258  linccl  48259  lincvalsng  48261  lincvalpr  48263  lincvalsc0  48266  linc0scn0  48268  lincdifsn  48269  linc1  48270  lincsum  48274  lincscm  48275  lspsslco  48282  snlindsntor  48316  lincresunit3lem2  48325  ldepsnlinclem1  48350  ldepsnlinclem2  48351  prelrrx2  48562  prelrrx2b  48563  rrx2xpref1o  48567  rrx2plord  48569  rrx2linesl  48592  oppcthin  48838  indthinc  48852  prsthinc  48854  elpglem3  48943