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  3314  rexeqbii  3315  rabeqi  3416  rabrabi  3422  reqabi  3426  elab2gw  3642  elab2g  3644  elrabf  3652  elrab3t  3655  elrab2  3659  cbvsbcw  3783  cbvsbcvw  3784  cbvsbc  3785  elin2  4162  elsymdif  4217  noel  4297  eltpg  4646  elunirab  4882  elintrab  4920  disjxiun  5099  exss  5418  otiunsndisj  5475  brabsb  5486  brabga  5489  epelg  5532  pofun  5557  elxp  5654  opeliunxp  5698  opeliun2xp  5699  bropaex12  5722  brab2a  5724  elcnv  5830  dmopabelb  5870  elrnmptg  5914  elres  5980  elimampt  6003  elrid  6006  rninxp  6140  elid  6160  elsuci  6389  elsucg  6390  elsuc2g  6391  elfv  6838  0fv  6884  opabiota  6925  dffv2  6938  fvopab3g  6945  fvmptex  6964  fvopab5  6983  fvn0ssdmfun  7028  fveqressseq  7033  f0cli  7052  fmptco  7083  fvrnressn  7115  funfvima  7186  elunirnALT  7208  fliftel  7266  eloprabga  7478  elrnmpo  7505  elimampo  7506  ovid  7510  offval  7642  sucexeloniOLD  7766  1st2val  7975  2nd2val  7976  bropopvvv  8046  bropfvvvv  8048  fsplit  8073  xporderlem  8083  frpoins3xpg  8096  frpoins3xp3g  8097  brtpos2  8188  frrlem8  8249  frrlem9  8250  frrlem10  8251  fprresex  8266  issmo  8294  smores3  8299  tfrlem7  8328  tfrlem9  8330  tfrlem9a  8331  tfr2b  8341  tfr2  8343  rdgsuc  8369  frsucmptn  8384  tz7.48-2  8387  el1o  8436  ord2eln012  8438  dif1o  8441  ondif2  8443  oawordeulem  8495  elecg  8692  brecop  8760  erovlem  8763  eceqoveq  8772  mapsncnv  8843  mptelixpg  8885  brsdom  8923  isfi  8924  enssdom  8925  brdom2  8930  xpcomco  9008  brsdom2  9042  en3lplem2  9542  cnfcom2lem  9630  brttrcl2  9643  ttrcltr  9645  rnttrcl  9651  epfrs  9660  r1limg  9700  r1ord  9709  r1ord3  9711  tz9.12lem3  9718  rankvaln  9728  r1elss  9735  rankpwi  9752  ssrankr1  9764  r1val3  9767  r1pw  9774  rankr1b  9793  djur  9848  djuunxp  9850  eldju2ndl  9853  eldju2ndr  9854  isnum2  9874  cardprclem  9908  infxpenlem  9942  alephcard  9999  alephnbtwn  10000  alephnbtwn2  10001  alephord2  10005  alephsdom  10015  dfac3  10050  dfac5lem2  10053  dfac5lem3  10054  dfac5lem5  10056  pwsdompw  10132  cfub  10178  cardcf  10181  cflecard  10182  cfle  10183  cflim2  10192  cofsmo  10198  cfidm  10204  isfin3  10225  isfin5  10228  isfin6  10229  sdom2en01  10231  fin23lem26  10254  fin23lem30  10271  isf32lem5  10286  itunitc1  10349  ituniiun  10351  axdc3lem3  10381  axcclem  10386  axdclem  10448  iunfo  10468  iundom2g  10469  cardidg  10477  konigthlem  10497  alephadd  10506  alephreg  10511  pwcfsdom  10512  cfpwsdom  10513  elgch  10551  fpwwe2lem11  10570  canth4  10576  wunex2  10667  r1tskina  10711  elni  10805  nlt1pi  10835  adderpq  10885  mulerpq  10886  recmulnq  10893  addsrpr  11004  mulsrpr  11005  opelcn  11058  opelreal  11059  elreal  11060  elreal2  11061  0ncn  11062  addcnsr  11064  mulcnsr  11065  xrlenlt  11215  elnn0  12420  elnnne0  12432  un0addcl  12451  un0mulcl  12452  elxnn0  12493  uztrn2  12788  elnnuz  12813  elnn0uz  12814  elq  12885  elxr  13052  elfzm1b  13539  elfz0lmr  13719  uzrdgfni  13899  fzennn  13909  ser0  13995  hash2pwpr  14417  iswrd  14456  pfxccatpfx1  14677  s3iunsndisj  14910  sumz  15664  sumss  15666  fsumcvg3  15671  abscvgcvg  15761  isumshft  15781  prodf1  15833  prodeq1i  15858  zprod  15879  prod1  15886  prodss  15889  prodsn  15904  prodsnf  15906  bpolydiflem  15996  bpoly2  15999  bpoly3  16000  bpoly4  16001  ruclem6  16179  divides  16200  dvdsflip  16263  pwp1fsum  16337  sadc0  16400  eulerthlem2  16728  prm23lt5  16761  4sqlem2  16896  4sqlem12  16903  vdwpc  16927  xpscf  17504  cidpropd  17651  oppcsect  17720  funcpropd  17844  natpropd  17921  dfinito2  17945  dftermo2  17946  initoeu2lem0  17955  arwhoma  17987  eldmcoa  18007  pospo  18284  psss  18521  ismgmn0  18551  gsumpropd2lem  18588  elefmndbas  18782  smndex1basss  18814  smndex1mgm  18816  pwmnd  18846  dfgrp2e  18877  mulgfval  18983  eqg0subg  19110  cycsubmel  19114  ghmeqker  19157  elcntr  19244  cntri  19246  cntzsgrpcl  19248  oppgsubg  19277  fvcosymgeq  19343  symgfixels  19348  pmtrfrn  19372  efgsfo  19653  efgrelexlemb  19664  lt6abl  19809  dmdprd  19914  dprdval  19919  dprdw  19926  srgbinomlem4  20149  isnirred  20340  isrhm  20398  issrng  20764  lspexchn2  21073  lspindp2l  21076  lspindp2  21077  lbsextlem2  21101  rnglidl1  21174  df2idl2  21199  2idlss  21204  rngqiprngimfo  21243  cnfldfun  21310  cnfldfunOLD  21323  pzriprnglem3  21425  pzriprnglem4  21426  pzriprnglem7  21429  pzriprnglem8  21430  pzriprnglem9  21431  pzriprnglem12  21434  pzriprnglem14  21436  dsmmelbas  21681  frlmbas3  21718  lindsind2  21761  islindf4  21780  psrbagf  21860  evlslem4  22016  psdmul  22086  ply1bascl2  22122  cply1mul  22216  lply1binom  22230  matsubgcell  22354  matinvgcell  22355  matvscacell  22356  matepmcl  22382  matepm2cl  22383  scmatscm  22433  smatvscl  22444  marrepcl  22484  marepvcl  22489  mulmarep1el  22492  mulmarep1gsum1  22493  mulmarep1gsum2  22494  submabas  22498  m1detdiag  22517  mdetdiag  22519  m2detleib  22551  gsummatr01lem3  22577  gsummatr01  22579  smadiadetlem4  22589  slesolinv  22600  slesolinvbi  22601  slesolex  22602  cramerimplem2  22604  pmatcoe1fsupp  22621  mat2pmatbas  22646  mat2pmatmul  22651  mat2pmatlin  22655  decpmatmul  22692  monmatcollpw  22699  pm2mpf1  22719  pm2mpghm  22736  istps  22854  mretopd  23012  neiptopuni  23050  lpdifsn  23063  restcls  23101  perfopn  23105  pnfnei  23140  mnfnei  23141  lmss  23218  hauscmplem  23326  is2ndc  23366  2ndcdisj  23376  hausnlly  23413  txuni2  23485  ptpjpre1  23491  elpt  23492  dfac14  23538  xkococn  23580  fbasrn  23804  fin1aufil  23852  elfm2  23868  elfm3  23870  fbflim  23896  flffbas  23915  cnpflf2  23920  fclsbas  23941  efmndtmd  24021  tsmssubm  24063  iscusp2  24222  imasdsf1olem  24294  metustel  24471  metuel2  24486  isnghm  24644  opnreen  24753  iccpnfcnv  24875  ehleudisval  25352  ehl1eudis  25353  ehl2eudis  25355  minveclem3b  25361  ovoliunlem1  25436  ioombl1lem4  25495  subopnmbl  25538  vitalilem2  25543  vitalilem3  25544  mbfimaopnlem  25589  mbfimaopn2  25591  itg2l  25663  dvply1  26224  vieta1lem1  26251  vieta1lem2  26252  elaa  26257  taylthlem2  26315  taylthlem2OLD  26316  abelthlem6  26379  abelthlem9  26383  sinq34lt0t  26451  ellogrn  26501  dvrelog  26579  ellogdm  26581  logtayl2  26604  cxpcn3lem  26690  cxpcn3  26691  1cubr  26785  atandm  26819  atanf  26823  reasinsin  26839  atans2  26874  dmarea  26900  xrlimcnp  26911  amgmlem  26933  ppiublem1  27146  lgsdir2lem2  27270  gausslemma2dlem1a  27309  lgsquadlem1  27324  lgsquadlem2  27325  2sqlem1  27361  rpvmasum2  27456  madeval2  27798  newval  27800  leftval  27808  rightval  27809  lltropt  27821  madess  27825  oldssmade  27826  oldss  27827  lrold  27846  addsproplem2  27917  addsproplem4  27919  addsproplem6  27921  negsproplem4  27977  negsproplem6  27979  precsexlem10  28158  precsexlem11  28159  sltonold  28202  elnns  28272  elzs  28312  edgiedgb  29034  isuhgr  29040  isushgr  29041  isupgr  29064  isumgr  29075  umgredg  29118  umgrpredgv  29120  umgredgne  29125  umgredgnlp  29127  isuspgr  29132  isusgr  29133  ausgrusgri  29148  usgredgppr  29176  edgssv2  29178  uspgredg2vlem  29203  uspgredg2v  29204  ushgredgedg  29209  ushgredgedgloop  29211  griedg0ssusgr  29245  uhgrissubgr  29255  subumgredg2  29265  uhgrspansubgrlem  29270  umgrres1lem  29290  upgrres1  29293  nbgrcl  29315  nbuhgr  29323  nbuhgr2vtx1edgblem  29331  nbupgrres  29344  edgnbusgreu  29347  nbusgredgeu0  29348  nbusgrf1o0  29349  hashnbusgrnn0  29356  nbupgruvtxres  29387  cffldtocusgr  29427  cffldtocusgrOLD  29428  cusgrfilem2  29437  vtxdg0v  29454  vtxduhgr0nedg  29473  uhgrvd00  29515  vtxdginducedm1  29524  finsumvtxdg2ssteplem4  29529  wlk1walk  29619  wlkp1lem6  29657  iswwlks  29816  wwlknllvtx  29826  wwlksonvtx  29835  wspthnonp  29839  wlkiswwlksupgr2  29857  wwlksnwwlksnon  29895  2pthon3v  29923  umgr2wlk  29929  elwwlks2s3  29931  wwlks2onv  29933  elwwlks2ons3im  29934  isclwwlk  29963  clwwlkccatlem  29968  clwlkclwwlk  29981  wwlksext2clwwlk  30036  hashecclwwlkn1  30056  umgrhashecclwwlk  30057  clwwlknon1  30076  clwwlknon1nloop  30078  clwwlknon2x  30082  1pthon2v  30132  uhgr3cyclex  30161  isconngr  30168  isconngr1  30169  eucrctshift  30222  frgrnbnb  30272  frgrncvvdeqlem1  30278  frgrncvvdeqlem2  30279  frgrncvvdeqlem3  30280  frgrncvvdeqlem9  30286  fusgreghash2wspv  30314  extwwlkfab  30331  numclwwlk1lem2foa  30333  numclwwlk1lem2fo  30337  clwlknon2num  30347  numclwlk2lem2f1o  30358  numclwwlk5lem  30366  topnfbey  30448  isvclem  30556  isnvlem  30589  vsfval  30612  h2hlm  30959  hhcmpl  31179  hhcms  31182  elch0  31233  omlsilem  31381  h1de2ctlem  31534  elspansni  31537  nonbooli  31630  spansncvi  31631  adjeq  31914  cnlnssadj  32059  cnvbraval  32089  brabgaf  32586  2ndresdju  32623  fmptdF  32630  fmptcof2  32631  acunirnmpt  32633  acunirnmpt2  32634  ofpreima  32639  fcnvgreu  32647  fdifsuppconst  32662  1stpreima  32680  2ndpreima  32681  fz2ssnn0  32758  elxrge02  32902  ccatws1f1o  32923  gsumwrd2dccatlem  33049  psgnfzto1stlem  33072  cycpmgcl  33125  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem4  33212  elrgspnsubrunlem1  33214  nsgqusf1olem2  33378  nsgqusf1olem3  33379  prmidl0  33414  crngmxidl  33433  opprnsg  33448  rprmirredb  33496  zringfrac  33518  evl1deg2  33539  evl1deg3  33540  ply1degltel  33553  ply1degleel  33554  fldextrspunlsplem  33661  isconstr  33719  constrsuc  33721  constrconj  33728  submatres  33789  lmat22lem  33800  crefdf  33831  cmppcmp  33841  rspectopn  33850  prsdm  33897  prsrn  33898  xrge0iifcnv  33916  xrge0iifiso  33918  xrge0iifhom  33920  pnfneige0  33934  qqhre  34003  rrhre  34004  esumnul  34031  esumcvgsum  34071  ldgenpisyslem1  34146  measvuni  34197  cntnevol  34211  dya2iocnrect  34265  sibf0  34318  oddpwdc  34338  eulerpartlemd  34350  eulerpartgbij  34356  eulerpartlemgh  34362  isrrvv  34427  coinfliprv  34467  ballotlem7  34520  signswch  34545  hashreprin  34604  chtvalz  34613  circlemethhgt  34627  hgt750lemb  34640  tgoldbachgt  34647  bnj23  34701  bnj158  34712  bnj168  34713  bnj1138  34771  bnj1143  34773  bnj1454  34825  bnj110  34841  bnj882  34909  bnj893  34911  bnj916  34916  bnj970  34930  bnj983  34934  bnj984  34935  bnj1137  34978  bnj1174  34986  bnj1388  35016  bnj1398  35017  onvf1odlem4  35086  loop1cycl  35117  subfacp1lem5  35164  satfv1  35343  satfrnmapom  35350  satf0op  35357  satf0n0  35358  fmlafvel  35365  fmlaomn0  35370  fmlan0  35371  satffunlem2lem2  35386  satfv0fvfmla0  35393  satefvfmla0  35398  mrsub0  35496  mrsubccat  35498  mrsubcn  35499  elmrsubrn  35500  msubco  35511  msubvrs  35540  elmthm  35556  mthmblem  35560  ellcsrspsn  35621  elrn3  35742  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  36228  fnessref  36338  bj-ififc  36563  bj-csbsnlem  36884  bj-elgab  36920  currysetlem1  36928  bj-eltag  36958  bj-sngltag  36964  bj-projun  36975  bj-velpwALT  37034  bj-0nelmpt  37097  bj-opelidres  37142  bj-inftyexpitaudisj  37186  bj-elccinfty  37195  f1omptsnlem  37317  icoreelrnab  37335  relowlpssretop  37345  rdgssun  37359  exrecfnlem  37360  finxpnom  37382  uncov  37588  tan2h  37599  ptrecube  37607  poimirlem25  37632  poimirlem29  37636  poimirlem30  37637  poimirlem31  37638  poimirlem32  37639  cnambfre  37655  ftc1cnnc  37679  sdclem2  37729  sdclem1  37730  fdc  37732  caushft  37748  issmgrpOLD  37850  ismndo  37859  isrngo  37884  isdivrngo  37937  csbcom2fi  38115  elecALTV  38248  brrabga  38316  eldmxrncnvepres  38389  eldmxrncnvepres2  38390  eldmcoss  38442  coss0  38463  elrels2  38470  dath  39723  diclspsn  41181  dvh4dimlem  41430  dvh2dim  41432  dvh3dim3N  41436  lcfrvalsnN  41528  mapdh6eN  41727  mapdh7dN  41737  mapdh8b  41767  hdmap1l6e  41801  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  42341  readvrec2  42342  readvrec  42343  frlmfielbas  42481  mhpind  42575  pellex  42816  rmspecnonsq  42888  islmodfg  43051  aaitgo  43144  areaquad  43198  ordeldif1o  43242  naddwordnexlem4  43383  fpwfvss  43394  finona1cl  43435  elcnvcnvintab  43564  elnonrel  43567  elcnvcnvlem  43581  cnvcnvintabd  43582  brfvrcld2  43674  grur1cld  44214  dvgrat  44294  cvgdvgrat  44295  radcnvrat  44296  nznngen  44298  uzmptshftfval  44328  binomcxplemcvg  44336  binomcxplemnotnn0  44338  tpid3gVD  44824  en3lplem2VD  44826  orbitclmpt  44941  wfaxrep  44977  wfaxsep  44978  wfaxpow  44980  wfaxpr  44981  wfaxun  44982  wfac8prim  44985  brpermmodelcnv  44987  nregmodellem  44999  iuneq1i  45072  rexanuz3  45083  eliuniin  45086  eliuniin2  45107  disjinfi  45179  fsneq  45193  iuneqfzuzlem  45323  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  47833  sclnbgrel  47840  isubgredg  47859  uhgrimedgi  47883  isuspgrim0  47887  isuspgrimlem  47888  gricushgr  47910  clnbgrgrimlem  47926  grimedg  47928  usgrgrtrirex  47942  stgrnbgr0  47956  isubgr3stgrlem3  47960  isubgr3stgrlem4  47961  isubgr3stgrlem6  47963  isubgr3stgrlem7  47964  uspgrlimlem2  47981  uspgrlimlem3  47982  grlimgrtrilem1  47986  grlimgrtrilem2  47987  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  48080  gpgprismgr4cycllem7  48084  gpgprismgr4cycllem8  48085  gpgprismgr4cycllem10  48087  pgnbgreunbgrlem3  48101  pgnbgreunbgrlem6  48107  pgnbgreunbgr  48108  uspgrsprf  48127  uspgrsprf1  48128  uspgrsprfo  48129  ply1sclrmsm  48365  lcoop  48393  lincfsuppcl  48395  linccl  48396  lincvalsng  48398  lincvalpr  48400  lincvalsc0  48403  linc0scn0  48405  lincdifsn  48406  linc1  48407  lincsum  48411  lincscm  48412  lspsslco  48419  snlindsntor  48453  lincresunit3lem2  48462  ldepsnlinclem1  48487  ldepsnlinclem2  48488  prelrrx2  48695  prelrrx2b  48696  rrx2xpref1o  48700  rrx2plord  48702  rrx2linesl  48725  sectrcl  49004  invrcl  49006  initopropdlemlem  49221  initopropd  49225  termopropd  49226  zeroopropd  49227  oppcthin  49420  indthinc  49444  prsthinc  49446  elpglem3  49695