Theorem eleq2i 2820

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 2817	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  eleq12i  2821  eleqtri  2826  eleq2s  2846  hbxfreq  2858  nfceqi  2888  raleqbii  3317  rexeqbii  3318  rabeqi  3419  rabrabi  3425  reqabi  3429  elab2gw  3645  elab2g  3647  elrabf  3655  elrab3t  3658  elrab2  3662  cbvsbcw  3786  cbvsbcvw  3787  cbvsbc  3788  elin2  4166  elsymdif  4221  noel  4301  eltpg  4650  elunirab  4886  elintrab  4924  disjxiun  5104  exss  5423  otiunsndisj  5480  brabsb  5491  brabga  5494  epelg  5539  pofun  5564  elxp  5661  opeliunxp  5705  opeliun2xp  5706  bropaex12  5730  brab2a  5732  elcnv  5840  dmopabelb  5880  elrnmptg  5925  elres  5991  elimampt  6014  elrid  6017  rninxp  6152  elid  6172  elsuci  6401  elsucg  6402  elsuc2g  6403  elfv  6856  0fv  6902  opabiota  6943  dffv2  6956  fvopab3g  6963  fvmptex  6982  fvopab5  7001  fvn0ssdmfun  7046  fveqressseq  7051  f0cli  7070  fmptco  7101  fvrnressn  7133  funfvima  7204  elunirnALT  7226  fliftel  7284  eloprabga  7498  elrnmpo  7525  elimampo  7526  ovid  7530  offval  7662  sucexeloniOLD  7786  1st2val  7996  2nd2val  7997  bropopvvv  8069  bropfvvvv  8071  fsplit  8096  xporderlem  8106  frpoins3xpg  8119  frpoins3xp3g  8120  brtpos2  8211  frrlem8  8272  frrlem9  8273  frrlem10  8274  fprresex  8289  issmo  8317  smores3  8322  tfrlem7  8351  tfrlem9  8353  tfrlem9a  8354  tfr2b  8364  tfr2  8366  rdgsuc  8392  frsucmptn  8407  tz7.48-2  8410  el1o  8459  ord2eln012  8461  dif1o  8464  ondif2  8466  oawordeulem  8518  elecg  8715  brecop  8783  erovlem  8786  eceqoveq  8795  mapsncnv  8866  mptelixpg  8908  brsdom  8946  isfi  8947  enssdom  8948  brdom2  8953  xpcomco  9031  brsdom2  9065  en3lplem2  9566  cnfcom2lem  9654  brttrcl2  9667  ttrcltr  9669  rnttrcl  9675  epfrs  9684  r1limg  9724  r1ord  9733  r1ord3  9735  tz9.12lem3  9742  rankvaln  9752  r1elss  9759  rankpwi  9776  ssrankr1  9788  r1val3  9791  r1pw  9798  rankr1b  9817  djur  9872  djuunxp  9874  eldju2ndl  9877  eldju2ndr  9878  isnum2  9898  cardprclem  9932  infxpenlem  9966  alephcard  10023  alephnbtwn  10024  alephnbtwn2  10025  alephord2  10029  alephsdom  10039  dfac3  10074  dfac5lem2  10077  dfac5lem3  10078  dfac5lem5  10080  pwsdompw  10156  cfub  10202  cardcf  10205  cflecard  10206  cfle  10207  cflim2  10216  cofsmo  10222  cfidm  10228  isfin3  10249  isfin5  10252  isfin6  10253  sdom2en01  10255  fin23lem26  10278  fin23lem30  10295  isf32lem5  10310  itunitc1  10373  ituniiun  10375  axdc3lem3  10405  axcclem  10410  axdclem  10472  iunfo  10492  iundom2g  10493  cardidg  10501  konigthlem  10521  alephadd  10530  alephreg  10535  pwcfsdom  10536  cfpwsdom  10537  elgch  10575  fpwwe2lem11  10594  canth4  10600  wunex2  10691  r1tskina  10735  elni  10829  nlt1pi  10859  adderpq  10909  mulerpq  10910  recmulnq  10917  addsrpr  11028  mulsrpr  11029  opelcn  11082  opelreal  11083  elreal  11084  elreal2  11085  0ncn  11086  addcnsr  11088  mulcnsr  11089  xrlenlt  11239  elnn0  12444  elnnne0  12456  un0addcl  12475  un0mulcl  12476  elxnn0  12517  uztrn2  12812  elnnuz  12837  elnn0uz  12838  elq  12909  elxr  13076  elfzm1b  13563  elfz0lmr  13743  uzrdgfni  13923  fzennn  13933  ser0  14019  hash2pwpr  14441  iswrd  14480  pfxccatpfx1  14701  s3iunsndisj  14934  sumz  15688  sumss  15690  fsumcvg3  15695  abscvgcvg  15785  isumshft  15805  prodf1  15857  prodeq1i  15882  zprod  15903  prod1  15910  prodss  15913  prodsn  15928  prodsnf  15930  bpolydiflem  16020  bpoly2  16023  bpoly3  16024  bpoly4  16025  ruclem6  16203  divides  16224  dvdsflip  16287  pwp1fsum  16361  sadc0  16424  eulerthlem2  16752  prm23lt5  16785  4sqlem2  16920  4sqlem12  16927  vdwpc  16951  xpscf  17528  cidpropd  17671  oppcsect  17740  funcpropd  17864  natpropd  17941  dfinito2  17965  dftermo2  17966  initoeu2lem0  17975  arwhoma  18007  eldmcoa  18027  pospo  18304  psss  18539  ismgmn0  18569  gsumpropd2lem  18606  elefmndbas  18800  smndex1basss  18832  smndex1mgm  18834  pwmnd  18864  dfgrp2e  18895  mulgfval  19001  eqg0subg  19128  cycsubmel  19132  ghmeqker  19175  elcntr  19262  cntri  19264  cntzsgrpcl  19266  oppgsubg  19295  fvcosymgeq  19359  symgfixels  19364  pmtrfrn  19388  efgsfo  19669  efgrelexlemb  19680  lt6abl  19825  dmdprd  19930  dprdval  19935  dprdw  19942  srgbinomlem4  20138  isnirred  20329  isrhm  20387  issrng  20753  lspexchn2  21041  lspindp2l  21044  lspindp2  21045  lbsextlem2  21069  rnglidl1  21142  df2idl2  21167  2idlss  21172  rngqiprngimfo  21211  cnfldfun  21278  cnfldfunOLD  21291  pzriprnglem3  21393  pzriprnglem4  21394  pzriprnglem7  21397  pzriprnglem8  21398  pzriprnglem9  21399  pzriprnglem12  21402  pzriprnglem14  21404  dsmmelbas  21648  frlmbas3  21685  lindsind2  21728  islindf4  21747  psrbagf  21827  evlslem4  21983  psdmul  22053  ply1bascl2  22089  cply1mul  22183  lply1binom  22197  matsubgcell  22321  matinvgcell  22322  matvscacell  22323  matepmcl  22349  matepm2cl  22350  scmatscm  22400  smatvscl  22411  marrepcl  22451  marepvcl  22456  mulmarep1el  22459  mulmarep1gsum1  22460  mulmarep1gsum2  22461  submabas  22465  m1detdiag  22484  mdetdiag  22486  m2detleib  22518  gsummatr01lem3  22544  gsummatr01  22546  smadiadetlem4  22556  slesolinv  22567  slesolinvbi  22568  slesolex  22569  cramerimplem2  22571  pmatcoe1fsupp  22588  mat2pmatbas  22613  mat2pmatmul  22618  mat2pmatlin  22622  decpmatmul  22659  monmatcollpw  22666  pm2mpf1  22686  pm2mpghm  22703  istps  22821  mretopd  22979  neiptopuni  23017  lpdifsn  23030  restcls  23068  perfopn  23072  pnfnei  23107  mnfnei  23108  lmss  23185  hauscmplem  23293  is2ndc  23333  2ndcdisj  23343  hausnlly  23380  txuni2  23452  ptpjpre1  23458  elpt  23459  dfac14  23505  xkococn  23547  fbasrn  23771  fin1aufil  23819  elfm2  23835  elfm3  23837  fbflim  23863  flffbas  23882  cnpflf2  23887  fclsbas  23908  efmndtmd  23988  tsmssubm  24030  iscusp2  24189  imasdsf1olem  24261  metustel  24438  metuel2  24453  isnghm  24611  opnreen  24720  iccpnfcnv  24842  ehleudisval  25319  ehl1eudis  25320  ehl2eudis  25322  minveclem3b  25328  ovoliunlem1  25403  ioombl1lem4  25462  subopnmbl  25505  vitalilem2  25510  vitalilem3  25511  mbfimaopnlem  25556  mbfimaopn2  25558  itg2l  25630  dvply1  26191  vieta1lem1  26218  vieta1lem2  26219  elaa  26224  taylthlem2  26282  taylthlem2OLD  26283  abelthlem6  26346  abelthlem9  26350  sinq34lt0t  26418  ellogrn  26468  dvrelog  26546  ellogdm  26548  logtayl2  26571  cxpcn3lem  26657  cxpcn3  26658  1cubr  26752  atandm  26786  atanf  26790  reasinsin  26806  atans2  26841  dmarea  26867  xrlimcnp  26878  amgmlem  26900  ppiublem1  27113  lgsdir2lem2  27237  gausslemma2dlem1a  27276  lgsquadlem1  27291  lgsquadlem2  27292  2sqlem1  27328  rpvmasum2  27423  madeval2  27761  newval  27763  leftval  27771  rightval  27772  lltropt  27784  madess  27788  oldssmade  27789  lrold  27808  addsproplem2  27877  addsproplem4  27879  addsproplem6  27881  negsproplem4  27937  negsproplem6  27939  precsexlem10  28118  precsexlem11  28119  sltonold  28162  elnns  28232  elzs  28272  edgiedgb  28981  isuhgr  28987  isushgr  28988  isupgr  29011  isumgr  29022  umgredg  29065  umgrpredgv  29067  umgredgne  29072  umgredgnlp  29074  isuspgr  29079  isusgr  29080  ausgrusgri  29095  usgredgppr  29123  edgssv2  29125  uspgredg2vlem  29150  uspgredg2v  29151  ushgredgedg  29156  ushgredgedgloop  29158  griedg0ssusgr  29192  uhgrissubgr  29202  subumgredg2  29212  uhgrspansubgrlem  29217  umgrres1lem  29237  upgrres1  29240  nbgrcl  29262  nbuhgr  29270  nbuhgr2vtx1edgblem  29278  nbupgrres  29291  edgnbusgreu  29294  nbusgredgeu0  29295  nbusgrf1o0  29296  hashnbusgrnn0  29303  nbupgruvtxres  29334  cffldtocusgr  29374  cffldtocusgrOLD  29375  cusgrfilem2  29384  vtxdg0v  29401  vtxduhgr0nedg  29420  uhgrvd00  29462  vtxdginducedm1  29471  finsumvtxdg2ssteplem4  29476  wlk1walk  29567  wlkp1lem6  29606  iswwlks  29766  wwlknllvtx  29776  wwlksonvtx  29785  wspthnonp  29789  wlkiswwlksupgr2  29807  wwlksnwwlksnon  29845  2pthon3v  29873  umgr2wlk  29879  elwwlks2s3  29881  wwlks2onv  29883  elwwlks2ons3im  29884  isclwwlk  29913  clwwlkccatlem  29918  clwlkclwwlk  29931  wwlksext2clwwlk  29986  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  clwwlknon1  30026  clwwlknon1nloop  30028  clwwlknon2x  30032  1pthon2v  30082  uhgr3cyclex  30111  isconngr  30118  isconngr1  30119  eucrctshift  30172  frgrnbnb  30222  frgrncvvdeqlem1  30228  frgrncvvdeqlem2  30229  frgrncvvdeqlem3  30230  frgrncvvdeqlem9  30236  fusgreghash2wspv  30264  extwwlkfab  30281  numclwwlk1lem2foa  30283  numclwwlk1lem2fo  30287  clwlknon2num  30297  numclwlk2lem2f1o  30308  numclwwlk5lem  30316  topnfbey  30398  isvclem  30506  isnvlem  30539  vsfval  30562  h2hlm  30909  hhcmpl  31129  hhcms  31132  elch0  31183  omlsilem  31331  h1de2ctlem  31484  elspansni  31487  nonbooli  31580  spansncvi  31581  adjeq  31864  cnlnssadj  32009  cnvbraval  32039  brabgaf  32536  2ndresdju  32573  fmptdF  32580  fmptcof2  32581  acunirnmpt  32583  acunirnmpt2  32584  ofpreima  32589  fcnvgreu  32597  fdifsuppconst  32612  1stpreima  32630  2ndpreima  32631  fz2ssnn0  32708  elxrge02  32852  ccatws1f1o  32873  gsumwrd2dccatlem  33006  psgnfzto1stlem  33057  cycpmgcl  33110  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem4  33196  elrgspnsubrunlem1  33198  nsgqusf1olem2  33385  nsgqusf1olem3  33386  prmidl0  33421  crngmxidl  33440  opprnsg  33455  rprmirredb  33503  zringfrac  33525  evl1deg2  33546  evl1deg3  33547  ply1degltel  33560  ply1degleel  33561  fldextrspunlsplem  33668  isconstr  33726  constrsuc  33728  constrconj  33735  submatres  33796  lmat22lem  33807  crefdf  33838  cmppcmp  33848  rspectopn  33857  prsdm  33904  prsrn  33905  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhom  33927  pnfneige0  33941  qqhre  34010  rrhre  34011  esumnul  34038  esumcvgsum  34078  ldgenpisyslem1  34153  measvuni  34204  cntnevol  34218  dya2iocnrect  34272  sibf0  34325  oddpwdc  34345  eulerpartlemd  34357  eulerpartgbij  34363  eulerpartlemgh  34369  isrrvv  34434  coinfliprv  34474  ballotlem7  34527  signswch  34552  hashreprin  34611  chtvalz  34620  circlemethhgt  34634  hgt750lemb  34647  tgoldbachgt  34654  bnj23  34708  bnj158  34719  bnj168  34720  bnj1138  34778  bnj1143  34780  bnj1454  34832  bnj110  34848  bnj882  34916  bnj893  34918  bnj916  34923  bnj970  34937  bnj983  34941  bnj984  34942  bnj1137  34985  bnj1174  34993  bnj1388  35023  bnj1398  35024  onvf1odlem4  35093  loop1cycl  35124  subfacp1lem5  35171  satfv1  35350  satfrnmapom  35357  satf0op  35364  satf0n0  35365  fmlafvel  35372  fmlaomn0  35377  fmlan0  35378  satffunlem2lem2  35393  satfv0fvfmla0  35400  satefvfmla0  35405  mrsub0  35503  mrsubccat  35505  mrsubcn  35506  elmrsubrn  35507  msubco  35518  msubvrs  35547  elmthm  35563  mthmblem  35567  ellcsrspsn  35628  elrn3  35749  dfon2lem7  35777  brsset  35877  eltrans  35879  elfix  35891  ellimits  35898  elfuns  35903  elsingles  35906  fvtransport  36020  brcolinear2  36046  fvray  36129  linedegen  36131  fvline  36132  ellines  36140  fwddifn0  36152  elhf  36162  hfninf  36174  rmoeqi  36175  rmoeqbii  36176  reueqi  36177  reueqbii  36178  rabeqbii  36182  iuneq12i  36183  iineq1i  36184  iineq12i  36185  riotaeqbii  36186  ixpeq1i  36188  itgeq12i  36194  cbvprodvw2  36235  fnessref  36345  bj-ififc  36570  bj-csbsnlem  36891  bj-elgab  36927  currysetlem1  36935  bj-eltag  36965  bj-sngltag  36971  bj-projun  36982  bj-velpwALT  37041  bj-0nelmpt  37104  bj-opelidres  37149  bj-inftyexpitaudisj  37193  bj-elccinfty  37202  f1omptsnlem  37324  icoreelrnab  37342  relowlpssretop  37352  rdgssun  37366  exrecfnlem  37367  finxpnom  37389  uncov  37595  tan2h  37606  ptrecube  37614  poimirlem25  37639  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  cnambfre  37662  ftc1cnnc  37686  sdclem2  37736  sdclem1  37737  fdc  37739  caushft  37755  issmgrpOLD  37857  ismndo  37866  isrngo  37891  isdivrngo  37944  csbcom2fi  38122  elecALTV  38255  brrabga  38323  eldmxrncnvepres  38396  eldmxrncnvepres2  38397  eldmcoss  38449  coss0  38470  elrels2  38477  dath  39730  diclspsn  41188  dvh4dimlem  41437  dvh2dim  41439  dvh3dim3N  41443  lcfrvalsnN  41535  mapdh6eN  41734  mapdh7dN  41744  mapdh8b  41774  hdmap1l6e  41808  lcmfunnnd  42000  3factsumint1  42009  primrootsunit1  42085  primrootscoprmpow  42087  aks6d1c2lem4  42115  sticksstones2  42135  sticksstones3  42136  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  aks6d1c6lem2  42159  aks6d1c6lem3  42160  redvmptabs  42348  readvrec2  42349  readvrec  42350  frlmfielbas  42488  mhpind  42582  pellex  42823  rmspecnonsq  42895  islmodfg  43058  aaitgo  43151  areaquad  43205  ordeldif1o  43249  naddwordnexlem4  43390  fpwfvss  43401  finona1cl  43442  elcnvcnvintab  43571  elnonrel  43574  elcnvcnvlem  43588  cnvcnvintabd  43589  brfvrcld2  43681  grur1cld  44221  dvgrat  44301  cvgdvgrat  44302  radcnvrat  44303  nznngen  44305  uzmptshftfval  44335  binomcxplemcvg  44343  binomcxplemnotnn0  44345  tpid3gVD  44831  en3lplem2VD  44833  orbitclmpt  44948  wfaxrep  44984  wfaxsep  44985  wfaxpow  44987  wfaxpr  44988  wfaxun  44989  wfac8prim  44992  brpermmodelcnv  44994  nregmodellem  45006  iuneq1i  45079  rexanuz3  45090  eliuniin  45093  eliuniin2  45114  disjinfi  45186  fsneq  45200  iuneqfzuzlem  45330  allbutfi  45389  eluzelz2  45399  uz0  45408  uzublem  45426  uzid3  45431  elicores  45531  uzinico  45557  climsuselem1  45605  climsuse  45606  islptre  45617  fnlimfvre  45672  limsupresico  45698  limsupvaluz  45706  limsupubuzlem  45710  limsupequzmptlem  45726  liminfresico  45769  cnrefiisplem  45827  stoweidlem14  46012  stoweidlem39  46037  stoweidlem48  46046  stoweidlem51  46049  stoweidlem59  46057  stoweidlem62  46060  wallispilem3  46065  fourierdlem42  46147  fourierdlem62  46166  fourierdlem80  46184  fourierdlem103  46207  fourierdlem104  46208  etransclem26  46258  rrxsnicc  46298  ioorrnopn  46303  ioorrnopnxr  46305  sge00  46374  sge0fodjrnlem  46414  sge0isum  46425  sge0seq  46444  meadjiunlem  46463  carageneld  46500  volicorescl  46551  hoidmv1lelem1  46589  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem3  46595  ovnhoilem2  46600  hoiqssbllem2  46621  opnvonmbllem2  46631  ovolval4lem1  46647  iinhoiicc  46672  vonioolem1  46678  smflimlem1  46769  smflimlem2  46770  smflim  46775  nsssmfmbf  46777  smfresal  46786  smfrec  46787  smfdiv  46795  smfpimbor1lem2  46797  smflim2  46804  smflimmpt  46808  smfinflem  46815  smflimsuplem1  46818  smflimsuplem2  46819  smflimsuplem3  46820  smflimsuplem5  46822  smflimsuplem6  46823  smflimsup  46826  smflimsupmpt  46827  smfliminfmpt  46830  tannpoly  46891  sinnpoly  46892  fcores  47068  ndmaovcl  47204  ndmaovcom  47206  ndmaovass  47207  ndmaovdistr  47208  dfatco  47257  otiunsndisjX  47280  fvmptrabdm  47294  ceilhalfelfzo1  47331  modmknepk  47363  elsetpreimafvb  47385  sprsymrelfolem2  47494  sprsymrelf  47496  sprsymrelf1  47497  prpair  47502  prproropf1olem0  47503  paireqne  47512  fmtno4prmfac  47573  dfodd5  47661  sbgoldbo  47788  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  clnbgrcl  47822  clnbgredg  47840  sclnbgrel  47847  isubgredg  47866  uhgrimedgi  47890  isuspgrim0  47894  isuspgrimlem  47895  gricushgr  47917  clnbgrgrimlem  47933  grimedg  47935  usgrgrtrirex  47949  stgrnbgr0  47963  isubgr3stgrlem3  47967  isubgr3stgrlem4  47968  isubgr3stgrlem6  47970  isubgr3stgrlem7  47971  uspgrlimlem2  47988  uspgrlimlem3  47989  grlimgrtrilem1  47993  grlimgrtrilem2  47994  usgrexmpl2trifr  48028  gpgvtxel  48038  gpgedgel  48041  gpgusgralem  48047  gpg5order  48051  gpgvtxedg0  48054  gpgvtxedg1  48055  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  gpg5nbgrvtx03star  48071  gpg5nbgr3star  48072  gpgvtxdg3  48073  gpg5gricstgr3  48081  gpgprismgr4cycllem3  48087  gpgprismgr4cycllem7  48091  gpgprismgr4cycllem8  48092  gpgprismgr4cycllem10  48094  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  pgnbgreunbgr  48115  uspgrsprf  48134  uspgrsprf1  48135  uspgrsprfo  48136  ply1sclrmsm  48372  lcoop  48400  lincfsuppcl  48402  linccl  48403  lincvalsng  48405  lincvalpr  48407  lincvalsc0  48410  linc0scn0  48412  lincdifsn  48413  linc1  48414  lincsum  48418  lincscm  48419  lspsslco  48426  snlindsntor  48460  lincresunit3lem2  48469  ldepsnlinclem1  48494  ldepsnlinclem2  48495  prelrrx2  48702  prelrrx2b  48703  rrx2xpref1o  48707  rrx2plord  48709  rrx2linesl  48732  sectrcl  49011  invrcl  49013  initopropdlemlem  49228  initopropd  49232  termopropd  49233  zeroopropd  49234  oppcthin  49427  indthinc  49451  prsthinc  49453  elpglem3  49702