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  3307  rexeqbii  3308  rabeqi  3408  rabrabi  3414  reqabi  3418  elab2gw  3634  elab2g  3636  elrabf  3644  elrab3t  3647  elrab2  3651  cbvsbcw  3775  cbvsbcvw  3776  cbvsbc  3777  elin2  4154  elsymdif  4209  noel  4289  eltpg  4638  elunirab  4873  elintrab  4910  disjxiun  5089  exss  5406  otiunsndisj  5463  brabsb  5474  brabga  5477  epelg  5520  pofun  5545  elxp  5642  opeliunxp  5686  opeliun2xp  5687  bropaex12  5710  brab2a  5712  elcnv  5819  dmopabelb  5859  elrnmptg  5903  elres  5971  elimampt  5994  elrid  5997  rninxp  6128  elid  6148  elsuci  6376  elsucg  6377  elsuc2g  6378  elfv  6820  0fv  6864  opabiota  6905  dffv2  6918  fvopab3g  6925  fvmptex  6944  fvopab5  6963  fvn0ssdmfun  7008  fveqressseq  7013  f0cli  7032  fmptco  7063  fvrnressn  7095  funfvima  7166  elunirnALT  7188  fliftel  7246  eloprabga  7458  elrnmpo  7485  elimampo  7486  ovid  7490  offval  7622  1st2val  7952  2nd2val  7953  bropopvvv  8023  bropfvvvv  8025  fsplit  8050  xporderlem  8060  frpoins3xpg  8073  frpoins3xp3g  8074  brtpos2  8165  frrlem8  8226  frrlem9  8227  frrlem10  8228  fprresex  8243  issmo  8271  smores3  8276  tfrlem7  8305  tfrlem9  8307  tfrlem9a  8308  tfr2b  8318  tfr2  8320  rdgsuc  8346  frsucmptn  8361  tz7.48-2  8364  el1o  8413  ord2eln012  8415  dif1o  8418  ondif2  8420  oawordeulem  8472  elecg  8669  brecop  8737  erovlem  8740  eceqoveq  8749  mapsncnv  8820  mptelixpg  8862  brsdom  8900  isfi  8901  enssdom  8902  brdom2  8907  xpcomco  8984  brsdom2  9018  en3lplem2  9509  cnfcom2lem  9597  brttrcl2  9610  ttrcltr  9612  rnttrcl  9618  epfrs  9627  r1limg  9667  r1ord  9676  r1ord3  9678  tz9.12lem3  9685  rankvaln  9695  r1elss  9702  rankpwi  9719  ssrankr1  9731  r1val3  9734  r1pw  9741  rankr1b  9760  djur  9815  djuunxp  9817  eldju2ndl  9820  eldju2ndr  9821  isnum2  9841  cardprclem  9875  infxpenlem  9907  alephcard  9964  alephnbtwn  9965  alephnbtwn2  9966  alephord2  9970  alephsdom  9980  dfac3  10015  dfac5lem2  10018  dfac5lem3  10019  dfac5lem5  10021  pwsdompw  10097  cfub  10143  cardcf  10146  cflecard  10147  cfle  10148  cflim2  10157  cofsmo  10163  cfidm  10169  isfin3  10190  isfin5  10193  isfin6  10194  sdom2en01  10196  fin23lem26  10219  fin23lem30  10236  isf32lem5  10251  itunitc1  10314  ituniiun  10316  axdc3lem3  10346  axcclem  10351  axdclem  10413  iunfo  10433  iundom2g  10434  cardidg  10442  konigthlem  10462  alephadd  10471  alephreg  10476  pwcfsdom  10477  cfpwsdom  10478  elgch  10516  fpwwe2lem11  10535  canth4  10541  wunex2  10632  r1tskina  10676  elni  10770  nlt1pi  10800  adderpq  10850  mulerpq  10851  recmulnq  10858  addsrpr  10969  mulsrpr  10970  opelcn  11023  opelreal  11024  elreal  11025  elreal2  11026  0ncn  11027  addcnsr  11029  mulcnsr  11030  xrlenlt  11180  elnn0  12386  elnnne0  12398  un0addcl  12417  un0mulcl  12418  elxnn0  12459  uztrn2  12754  elnnuz  12779  elnn0uz  12780  elq  12851  elxr  13018  elfzm1b  13505  elfz0lmr  13685  uzrdgfni  13865  fzennn  13875  ser0  13961  hash2pwpr  14383  iswrd  14422  pfxccatpfx1  14642  s3iunsndisj  14875  sumz  15629  sumss  15631  fsumcvg3  15636  abscvgcvg  15726  isumshft  15746  prodf1  15798  prodeq1i  15823  zprod  15844  prod1  15851  prodss  15854  prodsn  15869  prodsnf  15871  bpolydiflem  15961  bpoly2  15964  bpoly3  15965  bpoly4  15966  ruclem6  16144  divides  16165  dvdsflip  16228  pwp1fsum  16302  sadc0  16365  eulerthlem2  16693  prm23lt5  16726  4sqlem2  16861  4sqlem12  16868  vdwpc  16892  xpscf  17469  cidpropd  17616  oppcsect  17685  funcpropd  17809  natpropd  17886  dfinito2  17910  dftermo2  17911  initoeu2lem0  17920  arwhoma  17952  eldmcoa  17972  pospo  18249  psss  18486  ismgmn0  18516  gsumpropd2lem  18553  elefmndbas  18747  smndex1basss  18779  smndex1mgm  18781  pwmnd  18811  dfgrp2e  18842  mulgfval  18948  eqg0subg  19075  cycsubmel  19079  ghmeqker  19122  elcntr  19209  cntri  19211  cntzsgrpcl  19213  oppgsubg  19242  fvcosymgeq  19308  symgfixels  19313  pmtrfrn  19337  efgsfo  19618  efgrelexlemb  19629  lt6abl  19774  dmdprd  19879  dprdval  19884  dprdw  19891  srgbinomlem4  20114  isnirred  20305  isrhm  20363  issrng  20729  lspexchn2  21038  lspindp2l  21041  lspindp2  21042  lbsextlem2  21066  rnglidl1  21139  df2idl2  21164  2idlss  21169  rngqiprngimfo  21208  cnfldfun  21275  cnfldfunOLD  21288  pzriprnglem3  21390  pzriprnglem4  21391  pzriprnglem7  21394  pzriprnglem8  21395  pzriprnglem9  21396  pzriprnglem12  21399  pzriprnglem14  21401  dsmmelbas  21646  frlmbas3  21683  lindsind2  21726  islindf4  21745  psrbagf  21825  evlslem4  21981  psdmul  22051  ply1bascl2  22087  cply1mul  22181  lply1binom  22195  matsubgcell  22319  matinvgcell  22320  matvscacell  22321  matepmcl  22347  matepm2cl  22348  scmatscm  22398  smatvscl  22409  marrepcl  22449  marepvcl  22454  mulmarep1el  22457  mulmarep1gsum1  22458  mulmarep1gsum2  22459  submabas  22463  m1detdiag  22482  mdetdiag  22484  m2detleib  22516  gsummatr01lem3  22542  gsummatr01  22544  smadiadetlem4  22554  slesolinv  22565  slesolinvbi  22566  slesolex  22567  cramerimplem2  22569  pmatcoe1fsupp  22586  mat2pmatbas  22611  mat2pmatmul  22616  mat2pmatlin  22620  decpmatmul  22657  monmatcollpw  22664  pm2mpf1  22684  pm2mpghm  22701  istps  22819  mretopd  22977  neiptopuni  23015  lpdifsn  23028  restcls  23066  perfopn  23070  pnfnei  23105  mnfnei  23106  lmss  23183  hauscmplem  23291  is2ndc  23331  2ndcdisj  23341  hausnlly  23378  txuni2  23450  ptpjpre1  23456  elpt  23457  dfac14  23503  xkococn  23545  fbasrn  23769  fin1aufil  23817  elfm2  23833  elfm3  23835  fbflim  23861  flffbas  23880  cnpflf2  23885  fclsbas  23906  efmndtmd  23986  tsmssubm  24028  iscusp2  24187  imasdsf1olem  24259  metustel  24436  metuel2  24451  isnghm  24609  opnreen  24718  iccpnfcnv  24840  ehleudisval  25317  ehl1eudis  25318  ehl2eudis  25320  minveclem3b  25326  ovoliunlem1  25401  ioombl1lem4  25460  subopnmbl  25503  vitalilem2  25508  vitalilem3  25509  mbfimaopnlem  25554  mbfimaopn2  25556  itg2l  25628  dvply1  26189  vieta1lem1  26216  vieta1lem2  26217  elaa  26222  taylthlem2  26280  taylthlem2OLD  26281  abelthlem6  26344  abelthlem9  26348  sinq34lt0t  26416  ellogrn  26466  dvrelog  26544  ellogdm  26546  logtayl2  26569  cxpcn3lem  26655  cxpcn3  26656  1cubr  26750  atandm  26784  atanf  26788  reasinsin  26804  atans2  26839  dmarea  26865  xrlimcnp  26876  amgmlem  26898  ppiublem1  27111  lgsdir2lem2  27235  gausslemma2dlem1a  27274  lgsquadlem1  27289  lgsquadlem2  27290  2sqlem1  27326  rpvmasum2  27421  madeval2  27763  newval  27765  leftval  27773  rightval  27774  lltropt  27786  madess  27790  oldssmade  27791  oldss  27792  lrold  27811  addsproplem2  27882  addsproplem4  27884  addsproplem6  27886  negsproplem4  27942  negsproplem6  27944  precsexlem10  28123  precsexlem11  28124  sltonold  28167  elnns  28237  elzs  28277  edgiedgb  28999  isuhgr  29005  isushgr  29006  isupgr  29029  isumgr  29040  umgredg  29083  umgrpredgv  29085  umgredgne  29090  umgredgnlp  29092  isuspgr  29097  isusgr  29098  ausgrusgri  29113  usgredgppr  29141  edgssv2  29143  uspgredg2vlem  29168  uspgredg2v  29169  ushgredgedg  29174  ushgredgedgloop  29176  griedg0ssusgr  29210  uhgrissubgr  29220  subumgredg2  29230  uhgrspansubgrlem  29235  umgrres1lem  29255  upgrres1  29258  nbgrcl  29280  nbuhgr  29288  nbuhgr2vtx1edgblem  29296  nbupgrres  29309  edgnbusgreu  29312  nbusgredgeu0  29313  nbusgrf1o0  29314  hashnbusgrnn0  29321  nbupgruvtxres  29352  cffldtocusgr  29392  cffldtocusgrOLD  29393  cusgrfilem2  29402  vtxdg0v  29419  vtxduhgr0nedg  29438  uhgrvd00  29480  vtxdginducedm1  29489  finsumvtxdg2ssteplem4  29494  wlk1walk  29584  wlkp1lem6  29622  iswwlks  29781  wwlknllvtx  29791  wwlksonvtx  29800  wspthnonp  29804  wlkiswwlksupgr2  29822  wwlksnwwlksnon  29860  2pthon3v  29888  umgr2wlk  29894  elwwlks2s3  29896  wwlks2onv  29898  elwwlks2ons3im  29899  isclwwlk  29928  clwwlkccatlem  29933  clwlkclwwlk  29946  wwlksext2clwwlk  30001  hashecclwwlkn1  30021  umgrhashecclwwlk  30022  clwwlknon1  30041  clwwlknon1nloop  30043  clwwlknon2x  30047  1pthon2v  30097  uhgr3cyclex  30126  isconngr  30133  isconngr1  30134  eucrctshift  30187  frgrnbnb  30237  frgrncvvdeqlem1  30243  frgrncvvdeqlem2  30244  frgrncvvdeqlem3  30245  frgrncvvdeqlem9  30251  fusgreghash2wspv  30279  extwwlkfab  30296  numclwwlk1lem2foa  30298  numclwwlk1lem2fo  30302  clwlknon2num  30312  numclwlk2lem2f1o  30323  numclwwlk5lem  30331  topnfbey  30413  isvclem  30521  isnvlem  30554  vsfval  30577  h2hlm  30924  hhcmpl  31144  hhcms  31147  elch0  31198  omlsilem  31346  h1de2ctlem  31499  elspansni  31502  nonbooli  31595  spansncvi  31596  adjeq  31879  cnlnssadj  32024  cnvbraval  32054  brabgaf  32553  2ndresdju  32593  fmptdF  32600  fmptcof2  32601  acunirnmpt  32603  acunirnmpt2  32604  ofpreima  32609  fcnvgreu  32617  fdifsuppconst  32632  1stpreima  32650  2ndpreima  32651  fz2ssnn0  32729  elxrge02  32873  ccatws1f1o  32894  gsumwrd2dccatlem  33020  psgnfzto1stlem  33043  cycpmgcl  33096  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem4  33186  elrgspnsubrunlem1  33188  nsgqusf1olem2  33352  nsgqusf1olem3  33353  prmidl0  33388  crngmxidl  33407  opprnsg  33422  rprmirredb  33470  zringfrac  33492  evl1deg2  33513  evl1deg3  33514  ply1degltel  33528  ply1degleel  33529  fldextrspunlsplem  33646  isconstr  33709  constrsuc  33711  constrconj  33718  submatres  33779  lmat22lem  33790  crefdf  33821  cmppcmp  33831  rspectopn  33840  prsdm  33887  prsrn  33888  xrge0iifcnv  33906  xrge0iifiso  33908  xrge0iifhom  33910  pnfneige0  33924  qqhre  33993  rrhre  33994  esumnul  34021  esumcvgsum  34061  ldgenpisyslem1  34136  measvuni  34187  cntnevol  34201  dya2iocnrect  34255  sibf0  34308  oddpwdc  34328  eulerpartlemd  34340  eulerpartgbij  34346  eulerpartlemgh  34352  isrrvv  34417  coinfliprv  34457  ballotlem7  34510  signswch  34535  hashreprin  34594  chtvalz  34603  circlemethhgt  34617  hgt750lemb  34630  tgoldbachgt  34637  bnj23  34691  bnj158  34702  bnj168  34703  bnj1138  34761  bnj1143  34763  bnj1454  34815  bnj110  34831  bnj882  34899  bnj893  34901  bnj916  34906  bnj970  34920  bnj983  34924  bnj984  34925  bnj1137  34968  bnj1174  34976  bnj1388  35006  bnj1398  35007  onvf1odlem4  35089  loop1cycl  35120  subfacp1lem5  35167  satfv1  35346  satfrnmapom  35353  satf0op  35360  satf0n0  35361  fmlafvel  35368  fmlaomn0  35373  fmlan0  35374  satffunlem2lem2  35389  satfv0fvfmla0  35396  satefvfmla0  35401  mrsub0  35499  mrsubccat  35501  mrsubcn  35502  elmrsubrn  35503  msubco  35514  msubvrs  35543  elmthm  35559  mthmblem  35563  ellcsrspsn  35624  elrn3  35745  dfon2lem7  35773  brsset  35873  eltrans  35875  elfix  35887  ellimits  35894  elfuns  35899  elsingles  35902  fvtransport  36016  brcolinear2  36042  fvray  36125  linedegen  36127  fvline  36128  ellines  36136  fwddifn0  36148  elhf  36158  hfninf  36170  rmoeqi  36171  rmoeqbii  36172  reueqi  36173  reueqbii  36174  rabeqbii  36178  iuneq12i  36179  iineq1i  36180  iineq12i  36181  riotaeqbii  36182  ixpeq1i  36184  itgeq12i  36190  cbvprodvw2  36231  fnessref  36341  bj-ififc  36566  bj-csbsnlem  36887  bj-elgab  36923  currysetlem1  36931  bj-eltag  36961  bj-sngltag  36967  bj-projun  36978  bj-velpwALT  37037  bj-0nelmpt  37100  bj-opelidres  37145  bj-inftyexpitaudisj  37189  bj-elccinfty  37198  f1omptsnlem  37320  icoreelrnab  37338  relowlpssretop  37348  rdgssun  37362  exrecfnlem  37363  finxpnom  37385  uncov  37591  tan2h  37602  ptrecube  37610  poimirlem25  37635  poimirlem29  37639  poimirlem30  37640  poimirlem31  37641  poimirlem32  37642  cnambfre  37658  ftc1cnnc  37682  sdclem2  37732  sdclem1  37733  fdc  37735  caushft  37751  issmgrpOLD  37853  ismndo  37862  isrngo  37887  isdivrngo  37940  csbcom2fi  38118  elecALTV  38251  brrabga  38319  eldmxrncnvepres  38392  eldmxrncnvepres2  38393  eldmcoss  38445  coss0  38466  elrels2  38473  dath  39725  diclspsn  41183  dvh4dimlem  41432  dvh2dim  41434  dvh3dim3N  41438  lcfrvalsnN  41530  mapdh6eN  41729  mapdh7dN  41739  mapdh8b  41769  hdmap1l6e  41803  lcmfunnnd  41995  3factsumint1  42004  primrootsunit1  42080  primrootscoprmpow  42082  aks6d1c2lem4  42110  sticksstones2  42130  sticksstones3  42131  sticksstones10  42138  sticksstones12a  42140  sticksstones12  42141  aks6d1c6lem2  42154  aks6d1c6lem3  42155  redvmptabs  42343  readvrec2  42344  readvrec  42345  frlmfielbas  42483  mhpind  42577  pellex  42818  rmspecnonsq  42890  islmodfg  43052  aaitgo  43145  areaquad  43199  ordeldif1o  43243  naddwordnexlem4  43384  fpwfvss  43395  finona1cl  43436  elcnvcnvintab  43565  elnonrel  43568  elcnvcnvlem  43582  cnvcnvintabd  43583  brfvrcld2  43675  grur1cld  44215  dvgrat  44295  cvgdvgrat  44296  radcnvrat  44297  nznngen  44299  uzmptshftfval  44329  binomcxplemcvg  44337  binomcxplemnotnn0  44339  tpid3gVD  44825  en3lplem2VD  44827  orbitclmpt  44942  wfaxrep  44978  wfaxsep  44979  wfaxpow  44981  wfaxpr  44982  wfaxun  44983  wfac8prim  44986  brpermmodelcnv  44988  nregmodellem  45000  iuneq1i  45073  rexanuz3  45084  eliuniin  45087  eliuniin2  45108  disjinfi  45180  fsneq  45194  iuneqfzuzlem  45324  allbutfi  45382  eluzelz2  45392  uz0  45401  uzublem  45419  uzid3  45424  elicores  45524  uzinico  45550  climsuselem1  45598  climsuse  45599  islptre  45610  fnlimfvre  45665  limsupresico  45691  limsupvaluz  45699  limsupubuzlem  45703  limsupequzmptlem  45719  liminfresico  45762  cnrefiisplem  45820  stoweidlem14  46005  stoweidlem39  46030  stoweidlem48  46039  stoweidlem51  46042  stoweidlem59  46050  stoweidlem62  46053  wallispilem3  46058  fourierdlem42  46140  fourierdlem62  46159  fourierdlem80  46177  fourierdlem103  46200  fourierdlem104  46201  etransclem26  46251  rrxsnicc  46291  ioorrnopn  46296  ioorrnopnxr  46298  sge00  46367  sge0fodjrnlem  46407  sge0isum  46418  sge0seq  46437  meadjiunlem  46456  carageneld  46493  volicorescl  46544  hoidmv1lelem1  46582  hoidmv1le  46585  hoidmvlelem1  46586  hoidmvlelem3  46588  ovnhoilem2  46593  hoiqssbllem2  46614  opnvonmbllem2  46624  ovolval4lem1  46640  iinhoiicc  46665  vonioolem1  46671  smflimlem1  46762  smflimlem2  46763  smflim  46768  nsssmfmbf  46770  smfresal  46779  smfrec  46780  smfdiv  46788  smfpimbor1lem2  46790  smflim2  46797  smflimmpt  46801  smfinflem  46808  smflimsuplem1  46811  smflimsuplem2  46812  smflimsuplem3  46813  smflimsuplem5  46815  smflimsuplem6  46816  smflimsup  46819  smflimsupmpt  46820  smfliminfmpt  46823  tannpoly  46884  sinnpoly  46885  fcores  47061  ndmaovcl  47197  ndmaovcom  47199  ndmaovass  47200  ndmaovdistr  47201  dfatco  47250  otiunsndisjX  47273  fvmptrabdm  47287  ceilhalfelfzo1  47324  modmknepk  47356  elsetpreimafvb  47378  sprsymrelfolem2  47487  sprsymrelf  47489  sprsymrelf1  47490  prpair  47495  prproropf1olem0  47496  paireqne  47505  fmtno4prmfac  47566  dfodd5  47654  sbgoldbo  47781  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  clnbgrcl  47815  clnbgredg  47834  sclnbgrel  47841  isubgredg  47860  uhgrimedgi  47884  isuspgrim0  47888  isuspgrimlem  47889  gricushgr  47911  clnbgrgrimlem  47927  grimedg  47929  usgrgrtrirex  47944  stgrnbgr0  47958  isubgr3stgrlem3  47962  isubgr3stgrlem4  47963  isubgr3stgrlem6  47965  isubgr3stgrlem7  47966  uspgrlimlem2  47983  uspgrlimlem3  47984  grlimedgclnbgr  47989  grlimprclnbgr  47990  grlimprclnbgrvtx  47993  grlimgrtrilem2  47996  usgrexmpl2trifr  48031  gpgvtxel  48041  gpgedgel  48044  gpgusgralem  48050  gpg5order  48054  gpgvtxedg0  48057  gpgvtxedg1  48058  gpgnbgrvtx0  48068  gpgnbgrvtx1  48069  gpg5nbgrvtx03star  48074  gpg5nbgr3star  48075  gpgvtxdg3  48076  gpg5gricstgr3  48084  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem7  48095  gpgprismgr4cycllem8  48096  gpgprismgr4cycllem10  48098  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  pgnbgreunbgr  48119  uspgrsprf  48140  uspgrsprf1  48141  uspgrsprfo  48142  ply1sclrmsm  48378  lcoop  48406  lincfsuppcl  48408  linccl  48409  lincvalsng  48411  lincvalpr  48413  lincvalsc0  48416  linc0scn0  48418  lincdifsn  48419  linc1  48420  lincsum  48424  lincscm  48425  lspsslco  48432  snlindsntor  48466  lincresunit3lem2  48475  ldepsnlinclem1  48500  ldepsnlinclem2  48501  prelrrx2  48708  prelrrx2b  48709  rrx2xpref1o  48713  rrx2plord  48715  rrx2linesl  48738  sectrcl  49017  invrcl  49019  initopropdlemlem  49234  initopropd  49238  termopropd  49239  zeroopropd  49240  oppcthin  49433  indthinc  49457  prsthinc  49459  elpglem3  49708