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  32592  fmptdF  32599  fmptcof2  32600  acunirnmpt  32602  acunirnmpt2  32603  ofpreima  32608  fcnvgreu  32616  fdifsuppconst  32631  1stpreima  32649  2ndpreima  32650  fz2ssnn0  32728  elxrge02  32872  ccatws1f1o  32893  gsumwrd2dccatlem  33019  psgnfzto1stlem  33042  cycpmgcl  33095  elrgspnlem1  33182  elrgspnlem2  33183  elrgspnlem4  33185  elrgspnsubrunlem1  33187  nsgqusf1olem2  33351  nsgqusf1olem3  33352  prmidl0  33387  crngmxidl  33406  opprnsg  33421  rprmirredb  33469  zringfrac  33491  evl1deg2  33512  evl1deg3  33513  ply1degltel  33527  ply1degleel  33528  fldextrspunlsplem  33640  isconstr  33703  constrsuc  33705  constrconj  33712  submatres  33773  lmat22lem  33784  crefdf  33815  cmppcmp  33825  rspectopn  33834  prsdm  33881  prsrn  33882  xrge0iifcnv  33900  xrge0iifiso  33902  xrge0iifhom  33904  pnfneige0  33918  qqhre  33987  rrhre  33988  esumnul  34015  esumcvgsum  34055  ldgenpisyslem1  34130  measvuni  34181  cntnevol  34195  dya2iocnrect  34249  sibf0  34302  oddpwdc  34322  eulerpartlemd  34334  eulerpartgbij  34340  eulerpartlemgh  34346  isrrvv  34411  coinfliprv  34451  ballotlem7  34504  signswch  34529  hashreprin  34588  chtvalz  34597  circlemethhgt  34611  hgt750lemb  34624  tgoldbachgt  34631  bnj23  34685  bnj158  34696  bnj168  34697  bnj1138  34755  bnj1143  34757  bnj1454  34809  bnj110  34825  bnj882  34893  bnj893  34895  bnj916  34900  bnj970  34914  bnj983  34918  bnj984  34919  bnj1137  34962  bnj1174  34970  bnj1388  35000  bnj1398  35001  onvf1odlem4  35079  loop1cycl  35110  subfacp1lem5  35157  satfv1  35336  satfrnmapom  35343  satf0op  35350  satf0n0  35351  fmlafvel  35358  fmlaomn0  35363  fmlan0  35364  satffunlem2lem2  35379  satfv0fvfmla0  35386  satefvfmla0  35391  mrsub0  35489  mrsubccat  35491  mrsubcn  35492  elmrsubrn  35493  msubco  35504  msubvrs  35533  elmthm  35549  mthmblem  35553  ellcsrspsn  35614  elrn3  35735  dfon2lem7  35763  brsset  35863  eltrans  35865  elfix  35877  ellimits  35884  elfuns  35889  elsingles  35892  fvtransport  36006  brcolinear2  36032  fvray  36115  linedegen  36117  fvline  36118  ellines  36126  fwddifn0  36138  elhf  36148  hfninf  36160  rmoeqi  36161  rmoeqbii  36162  reueqi  36163  reueqbii  36164  rabeqbii  36168  iuneq12i  36169  iineq1i  36170  iineq12i  36171  riotaeqbii  36172  ixpeq1i  36174  itgeq12i  36180  cbvprodvw2  36221  fnessref  36331  bj-ififc  36556  bj-csbsnlem  36877  bj-elgab  36913  currysetlem1  36921  bj-eltag  36951  bj-sngltag  36957  bj-projun  36968  bj-velpwALT  37027  bj-0nelmpt  37090  bj-opelidres  37135  bj-inftyexpitaudisj  37179  bj-elccinfty  37188  f1omptsnlem  37310  icoreelrnab  37328  relowlpssretop  37338  rdgssun  37352  exrecfnlem  37353  finxpnom  37375  uncov  37581  tan2h  37592  ptrecube  37600  poimirlem25  37625  poimirlem29  37629  poimirlem30  37630  poimirlem31  37631  poimirlem32  37632  cnambfre  37648  ftc1cnnc  37672  sdclem2  37722  sdclem1  37723  fdc  37725  caushft  37741  issmgrpOLD  37843  ismndo  37852  isrngo  37877  isdivrngo  37930  csbcom2fi  38108  elecALTV  38241  brrabga  38309  eldmxrncnvepres  38382  eldmxrncnvepres2  38383  eldmcoss  38435  coss0  38456  elrels2  38463  dath  39715  diclspsn  41173  dvh4dimlem  41422  dvh2dim  41424  dvh3dim3N  41428  lcfrvalsnN  41520  mapdh6eN  41719  mapdh7dN  41729  mapdh8b  41759  hdmap1l6e  41793  lcmfunnnd  41985  3factsumint1  41994  primrootsunit1  42070  primrootscoprmpow  42072  aks6d1c2lem4  42100  sticksstones2  42120  sticksstones3  42121  sticksstones10  42128  sticksstones12a  42130  sticksstones12  42131  aks6d1c6lem2  42144  aks6d1c6lem3  42145  redvmptabs  42333  readvrec2  42334  readvrec  42335  frlmfielbas  42473  mhpind  42567  pellex  42808  rmspecnonsq  42880  islmodfg  43042  aaitgo  43135  areaquad  43189  ordeldif1o  43233  naddwordnexlem4  43374  fpwfvss  43385  finona1cl  43426  elcnvcnvintab  43555  elnonrel  43558  elcnvcnvlem  43572  cnvcnvintabd  43573  brfvrcld2  43665  grur1cld  44205  dvgrat  44285  cvgdvgrat  44286  radcnvrat  44287  nznngen  44289  uzmptshftfval  44319  binomcxplemcvg  44327  binomcxplemnotnn0  44329  tpid3gVD  44815  en3lplem2VD  44817  orbitclmpt  44932  wfaxrep  44968  wfaxsep  44969  wfaxpow  44971  wfaxpr  44972  wfaxun  44973  wfac8prim  44976  brpermmodelcnv  44978  nregmodellem  44990  iuneq1i  45063  rexanuz3  45074  eliuniin  45077  eliuniin2  45098  disjinfi  45170  fsneq  45184  iuneqfzuzlem  45314  allbutfi  45372  eluzelz2  45382  uz0  45391  uzublem  45409  uzid3  45414  elicores  45514  uzinico  45540  climsuselem1  45588  climsuse  45589  islptre  45600  fnlimfvre  45655  limsupresico  45681  limsupvaluz  45689  limsupubuzlem  45693  limsupequzmptlem  45709  liminfresico  45752  cnrefiisplem  45810  stoweidlem14  45995  stoweidlem39  46020  stoweidlem48  46029  stoweidlem51  46032  stoweidlem59  46040  stoweidlem62  46043  wallispilem3  46048  fourierdlem42  46130  fourierdlem62  46149  fourierdlem80  46167  fourierdlem103  46190  fourierdlem104  46191  etransclem26  46241  rrxsnicc  46281  ioorrnopn  46286  ioorrnopnxr  46288  sge00  46357  sge0fodjrnlem  46397  sge0isum  46408  sge0seq  46427  meadjiunlem  46446  carageneld  46483  volicorescl  46534  hoidmv1lelem1  46572  hoidmv1le  46575  hoidmvlelem1  46576  hoidmvlelem3  46578  ovnhoilem2  46583  hoiqssbllem2  46604  opnvonmbllem2  46614  ovolval4lem1  46630  iinhoiicc  46655  vonioolem1  46661  smflimlem1  46752  smflimlem2  46753  smflim  46758  nsssmfmbf  46760  smfresal  46769  smfrec  46770  smfdiv  46778  smfpimbor1lem2  46780  smflim2  46787  smflimmpt  46791  smfinflem  46798  smflimsuplem1  46801  smflimsuplem2  46802  smflimsuplem3  46803  smflimsuplem5  46805  smflimsuplem6  46806  smflimsup  46809  smflimsupmpt  46810  smfliminfmpt  46813  tannpoly  46874  sinnpoly  46875  fcores  47051  ndmaovcl  47187  ndmaovcom  47189  ndmaovass  47190  ndmaovdistr  47191  dfatco  47240  otiunsndisjX  47263  fvmptrabdm  47277  ceilhalfelfzo1  47314  modmknepk  47346  elsetpreimafvb  47368  sprsymrelfolem2  47477  sprsymrelf  47479  sprsymrelf1  47480  prpair  47485  prproropf1olem0  47486  paireqne  47495  fmtno4prmfac  47556  dfodd5  47644  sbgoldbo  47771  nnsum4primeseven  47784  nnsum4primesevenALTV  47785  clnbgrcl  47805  clnbgredg  47824  sclnbgrel  47831  isubgredg  47850  uhgrimedgi  47874  isuspgrim0  47878  isuspgrimlem  47879  gricushgr  47901  clnbgrgrimlem  47917  grimedg  47919  usgrgrtrirex  47934  stgrnbgr0  47948  isubgr3stgrlem3  47952  isubgr3stgrlem4  47953  isubgr3stgrlem6  47955  isubgr3stgrlem7  47956  uspgrlimlem2  47973  uspgrlimlem3  47974  grlimedgclnbgr  47979  grlimprclnbgr  47980  grlimprclnbgrvtx  47983  grlimgrtrilem2  47986  usgrexmpl2trifr  48021  gpgvtxel  48031  gpgedgel  48034  gpgusgralem  48040  gpg5order  48044  gpgvtxedg0  48047  gpgvtxedg1  48048  gpgnbgrvtx0  48058  gpgnbgrvtx1  48059  gpg5nbgrvtx03star  48064  gpg5nbgr3star  48065  gpgvtxdg3  48066  gpg5gricstgr3  48074  gpgprismgr4cycllem3  48081  gpgprismgr4cycllem7  48085  gpgprismgr4cycllem8  48086  gpgprismgr4cycllem10  48088  pgnbgreunbgrlem3  48102  pgnbgreunbgrlem6  48108  pgnbgreunbgr  48109  uspgrsprf  48130  uspgrsprf1  48131  uspgrsprfo  48132  ply1sclrmsm  48368  lcoop  48396  lincfsuppcl  48398  linccl  48399  lincvalsng  48401  lincvalpr  48403  lincvalsc0  48406  linc0scn0  48408  lincdifsn  48409  linc1  48410  lincsum  48414  lincscm  48415  lspsslco  48422  snlindsntor  48456  lincresunit3lem2  48465  ldepsnlinclem1  48490  ldepsnlinclem2  48491  prelrrx2  48698  prelrrx2b  48699  rrx2xpref1o  48703  rrx2plord  48705  rrx2linesl  48728  sectrcl  49007  invrcl  49009  initopropdlemlem  49224  initopropd  49228  termopropd  49229  zeroopropd  49230  oppcthin  49423  indthinc  49447  prsthinc  49449  elpglem3  49698