Theorem eleq2i 2861

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

Syntax hints:   ↔ wb 209   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  eleq12i  2862  eleqtri  2867  eleq2s  2887  hbxfreq  2899  nfceqi  2928  raleqbii  3343  rexeqbii  3344  rabeqi  3436  rabrabi  3442  reqabi  3446  elab2gw  3646  elab2g  3648  elrabf  3656  elrab3t  3658  elrab2  3663  cbvsbcw  3786  cbvsbcvw  3787  cbvsbc  3788  elin2  4164  elsymdif  4219  noel  4299  eltpg  4657  elunirab  4891  elintrab  4929  disjxiun  5110  exss  5445  otiunsndisj  5504  brabsb  5516  brabga  5519  epelg  5563  pofun  5588  elxp  5685  opeliunxp  5729  opeliun2xp  5730  bropaex12  5753  brab2a  5755  elcnv  5863  cnv0  5870  dmopabelb  5907  elrnmptg  5952  elres  6020  elimampt  6046  elrid  6049  rninxp  6178  elid  6199  elsuci  6431  elsucg  6432  elsuc2g  6433  elfv  6880  0fv  6923  opabiota  6964  dffv2  6977  fvopab3g  6985  fvmptex  7005  fvopab5  7024  fsneq  7031  fvn0ssdmfun  7070  fveqressseq  7075  f0cli  7094  fmptco  7126  fvrnressn  7159  funfvima  7229  elunirnALT  7251  fliftel  7308  eloprabga  7520  elrnmpo  7547  elimampo  7548  ovid  7552  offval  7684  1st2val  8014  2nd2val  8015  bropopvvv  8085  bropfvvvv  8087  fsplit  8112  xporderlem  8123  frpoins3xpg  8136  frpoins3xp3g  8137  brtpos2  8228  frrlem8  8290  frrlem9  8291  frrlem10  8292  fprresex  8307  issmo  8335  smores3  8340  tfrlem7  8370  tfrlem9  8372  tfrlem9a  8373  tfr2b  8383  tfr2  8385  rdgsuc  8411  frsucmptn  8426  tz7.48-2  8429  el1o  8480  ord2eln012  8482  dif1o  8485  ondif2  8487  oawordeulem  8539  elecg  8739  brecop  8808  erovlem  8811  eceqoveq  8820  mapsncnv  8891  mptelixpg  8933  brsdom  8971  isfi  8972  enssdomOLD  8974  brdom2  8979  xpcomco  9055  brsdom2  9089  en3lplem2  9582  cnfcom2lem  9670  brttrcl2  9683  ttrcltr  9685  rnttrcl  9691  epfrs  9700  r1limg  9743  r1ord  9752  r1ord3  9754  tz9.12lem3  9761  rankvaln  9771  r1elss  9778  rankpwi  9795  ssrankr1  9807  r1val3  9810  r1pw  9817  rankr1b  9836  djur  9905  djuunxp  9907  eldju2ndl  9910  eldju2ndr  9911  isnum2  9931  cardprclem  9965  infxpenlem  9997  alephcard  10054  alephnbtwn  10055  alephnbtwn2  10056  alephord2  10060  alephsdom  10070  dfac3  10105  dfac5lem2  10108  dfac5lem3  10109  dfac5lem5  10111  pwsdompw  10186  cfub  10232  cardcf  10235  cflecard  10236  cfle  10237  cflim2  10247  cofsmo  10253  cfidm  10259  isfin3  10280  isfin5  10283  isfin6  10284  sdom2en01  10286  fin23lem26  10309  fin23lem30  10326  isf32lem5  10341  itunitc1  10404  ituniiun  10406  axdc3lem3  10436  axcclem  10441  axdclem  10503  iunfo  10523  iundom2g  10524  cardidg  10532  konigthlem  10553  alephadd  10562  alephreg  10567  pwcfsdom  10568  cfpwsdom  10569  elgch  10607  fpwwe2lem11  10626  canth4  10632  wunex2  10723  r1tskina  10767  elni  10861  nlt1pi  10891  adderpq  10941  mulerpq  10942  recmulnq  10949  addsrpr  11060  mulsrpr  11061  opelcn  11114  opelreal  11115  elreal  11116  elreal2  11117  0ncn  11118  addcnsr  11120  mulcnsr  11121  xrlenlt  11274  elnn0  12506  elnnne0  12518  un0addcl  12537  un0mulcl  12538  elxnn0  12579  uztrn2  12881  elnnuz  12902  elnn0uz  12903  elq  12974  elxr  13141  elfzm1b  13630  elfz0lmr  13812  uzrdgfni  13994  fzennn  14004  ser0  14090  hash2pwpr  14513  iswrd  14552  pfxccatpfx1  14773  s3iunsndisj  15005  sumz  15773  sumss  15775  fsumcvg3  15780  abscvgcvg  15871  isumshft  15893  prodf1  15945  prodeq1i  15970  zprod  15991  prod1  15998  prodss  16001  prodsn  16016  prodsnf  16018  bpolydiflem  16108  bpoly2  16111  bpoly3  16112  bpoly4  16113  ruclem6  16291  divides  16312  dvdsflip  16375  pwp1fsum  16449  sadc0  16512  eulerthlem2  16841  prm23lt5  16874  4sqlem2  17009  4sqlem12  17016  vdwpc  17040  xpscf  17619  cidpropd  17766  oppcsect  17835  funcpropd  17959  natpropd  18036  dfinito2  18060  dftermo2  18061  initoeu2lem0  18070  arwhoma  18102  eldmcoa  18122  pospo  18399  psss  18636  ex-chn1  18693  ex-chn2  18694  ismgmn0  18700  gsumpropd2lem  18737  elefmndbas  18932  smndex1basss  18967  smndex1mgm  18969  pwmnd  18999  dfgrp2e  19030  mulgfval  19135  eqg0subg  19267  cycsubmel  19271  ghmeqker  19313  elcntr  19400  cntri  19402  cntzsgrpcl  19404  oppgsubg  19433  fvcosymgeq  19499  symgfixels  19504  pmtrfrn  19528  efgsfo  19809  efgrelexlemb  19820  lt6abl  19965  dmdprd  20070  dprdval  20075  dprdw  20082  srgbinomlem4  20311  isnirred  20502  isrhm  20560  issrng  20925  lspexchn2  21233  lspindp2l  21236  lspindp2  21237  lbsextlem2  21261  rnglidl1  21336  df2idl2  21367  2idlss  21372  rngqiprngimfo  21412  prmidl0  21447  cnfldfun  21505  pzriprnglem3  21602  pzriprnglem4  21603  pzriprnglem7  21606  pzriprnglem8  21607  pzriprnglem9  21608  pzriprnglem12  21611  pzriprnglem14  21613  dsmmelbas  21858  frlmbas3  21895  lindsind2  21938  islindf4  21957  psrbagf  22037  evlslem4  22196  psdmul  22298  ply1bascl2  22333  cply1mul  22425  lply1binom  22439  matsubgcell  22560  matinvgcell  22561  matvscacell  22562  matepmcl  22588  matepm2cl  22589  scmatscm  22639  smatvscl  22650  marrepcl  22690  marepvcl  22695  mulmarep1el  22698  mulmarep1gsum1  22699  mulmarep1gsum2  22700  submabas  22704  m1detdiag  22723  mdetdiag  22725  m2detleib  22757  gsummatr01lem3  22783  gsummatr01  22785  smadiadetlem4  22795  slesolinv  22806  slesolinvbi  22807  slesolex  22808  cramerimplem2  22810  pmatcoe1fsupp  22827  mat2pmatbas  22852  mat2pmatmul  22857  mat2pmatlin  22861  decpmatmul  22898  monmatcollpw  22905  pm2mpf1  22925  pm2mpghm  22942  istps  23060  mretopd  23218  neiptopuni  23256  lpdifsn  23269  restcls  23307  perfopn  23311  pnfnei  23346  mnfnei  23347  lmss  23424  hauscmplem  23532  is2ndc  23572  2ndcdisj  23582  hausnlly  23619  txuni2  23691  ptpjpre1  23697  elpt  23698  dfac14  23744  xkococn  23786  fbasrn  24010  fin1aufil  24058  elfm2  24074  elfm3  24076  fbflim  24102  flffbas  24121  cnpflf2  24126  fclsbas  24147  efmndtmd  24227  tsmssubm  24269  iscusp2  24427  imasdsf1olem  24499  metustel  24676  metuel2  24691  isnghm  24849  opnreen  24958  iccpnfcnv  25072  ehleudisval  25547  ehl1eudis  25548  ehl2eudis  25550  minveclem3b  25556  ovoliunlem1  25630  ioombl1lem4  25689  subopnmbl  25732  vitalilem2  25737  vitalilem3  25738  mbfimaopnlem  25783  mbfimaopn2  25785  itg2l  25857  dvply1  26414  vieta1lem1  26440  vieta1lem2  26441  elaa  26446  taylthlem2  26503  abelthlem6  26565  abelthlem9  26569  sinq34lt0t  26640  ellogrn  26690  dvrelog  26768  ellogdm  26770  logtayl2  26793  cxpcn3lem  26878  cxpcn3  26879  1cubr  26973  atandm  27007  atanf  27011  reasinsin  27027  atans2  27062  dmarea  27088  xrlimcnp  27099  amgmlem  27120  ppiublem1  27332  lgsdir2lem2  27456  gausslemma2dlem1a  27495  lgsquadlem1  27510  lgsquadlem2  27511  2sqlem1  27547  rpvmasum2  27642  madeval2  27992  newval  27994  leftval  28008  rightval  28009  lltr  28021  madess  28025  oldssmade  28026  oldss  28029  lrold  28056  addsproplem2  28129  addsproplem4  28131  addsproplem6  28133  negsproplem4  28190  negsproplem6  28192  precsexlem10  28375  precsexlem11  28376  ltonold  28420  elnns  28499  elzs  28543  edgiedgb  29345  isuhgr  29351  isushgr  29352  isupgr  29375  isumgr  29386  umgredg  29429  umgrpredgv  29431  umgredgne  29436  umgredgnlp  29438  isuspgr  29443  isusgr  29444  ausgrusgri  29459  usgredgppr  29487  edgssv2  29489  uspgredg2vlem  29514  uspgredg2v  29515  ushgredgedg  29520  ushgredgedgloop  29522  griedg0ssusgr  29556  uhgrissubgr  29566  subumgredg2  29576  uhgrspansubgrlem  29581  umgrres1lem  29601  upgrres1  29604  nbgrcl  29626  nbuhgr  29634  nbuhgr2vtx1edgblem  29642  nbupgrres  29655  edgnbusgreu  29658  nbusgredgeu0  29659  nbusgrf1o0  29660  hashnbusgrnn0  29667  nbupgruvtxres  29698  cffldtocusgr  29738  cusgrfilem2  29747  vtxdg0v  29764  vtxduhgr0nedg  29783  uhgrvd00  29825  vtxdginducedm1  29834  finsumvtxdg2ssteplem4  29839  wlk1walk  29929  wlkp1lem6  29967  iswwlks  30126  wwlknllvtx  30136  wwlksonvtx  30145  wspthnonp  30149  wlkiswwlksupgr2  30167  wwlksnwwlksnon  30205  2pthon3v  30233  umgr2wlk  30239  elwwlks2s3  30241  wwlks2onv  30243  elwwlks2ons3im  30244  isclwwlk  30276  clwwlkccatlem  30281  clwlkclwwlk  30294  wwlksext2clwwlk  30349  hashecclwwlkn1  30369  umgrhashecclwwlk  30370  clwwlknon1  30389  clwwlknon1nloop  30391  clwwlknon2x  30395  1pthon2v  30445  uhgr3cyclex  30474  isconngr  30481  isconngr1  30482  eucrctshift  30535  frgrnbnb  30585  frgrncvvdeqlem1  30591  frgrncvvdeqlem2  30592  frgrncvvdeqlem3  30593  frgrncvvdeqlem9  30599  fusgreghash2wspv  30627  extwwlkfab  30644  numclwwlk1lem2foa  30646  numclwwlk1lem2fo  30650  clwlknon2num  30660  numclwlk2lem2f1o  30671  numclwwlk5lem  30679  topnfbey  30761  isvclem  30870  isnvlem  30903  vsfval  30926  h2hlm  31273  hhcmpl  31493  hhcms  31496  elch0  31547  omlsilem  31695  h1de2ctlem  31848  elspansni  31851  nonbooli  31944  spansncvi  31945  adjeq  32228  cnlnssadj  32373  cnvbraval  32403  brabgaf  32892  2ndresdju  32935  fmptdF  32942  fmptcof2  32943  acunirnmpt  32945  acunirnmpt2  32946  ofpreima  32951  fcnvgreu  32958  fdifsuppconst  32975  1stpreima  32993  2ndpreima  32994  fz2ssnn0  33071  elxrge02  33192  ccatws1f1o  33212  gsumwrd2dccatlem  33338  psgnfzto1stlem  33361  cycpmgcl  33414  elrgspnlem1  33503  elrgspnlem2  33504  elrgspnlem4  33506  elrgspnsubrunlem1  33508  rlocisunit  33537  domnprodeq0  33540  nsgqusf1olem2  33667  nsgqusf1olem3  33668  crngmxidl  33697  opprnsg  33711  rprmirredb  33767  zringfrac  33789  evl1deg2  33812  evl1deg3  33813  ply1degltel  33829  ply1degleel  33830  evlextv  33877  esplyfval3  33907  esplyindfv  33911  esplyfvn  33912  vietalem  33914  fldextrspunlsplem  34008  isconstr  34071  constrsuc  34073  constrconj  34080  submatres  34141  lmat22lem  34152  crefdf  34183  cmppcmp  34193  rspectopn  34202  prsdm  34249  prsrn  34250  xrge0iifcnv  34268  xrge0iifiso  34270  xrge0iifhom  34272  pnfneige0  34286  qqhre  34355  rrhre  34356  esumnul  34383  esumcvgsum  34423  ldgenpisyslem1  34498  measvuni  34549  cntnevol  34563  dya2iocnrect  34616  sibf0  34669  oddpwdc  34689  eulerpartlemd  34701  eulerpartgbij  34707  eulerpartlemgh  34713  isrrvv  34778  coinfliprv  34818  ballotlem7  34871  signswch  34893  hashreprin  34952  chtvalz  34961  circlemethhgt  34975  hgt750lemb  34988  tgoldbachgt  34995  bnj23  35052  bnj158  35063  bnj168  35064  bnj1138  35122  bnj1143  35123  bnj1454  35175  bnj110  35191  bnj882  35259  bnj893  35261  bnj916  35266  bnj970  35280  bnj983  35284  bnj984  35285  bnj1137  35328  bnj1174  35336  bnj1388  35366  bnj1398  35367  r1wf  35432  onvf1odlem4  35489  loop1cycl  35528  subfacp1lem5  35575  satfv1  35754  satfrnmapom  35761  satf0op  35768  satf0n0  35769  fmlafvel  35776  fmlaomn0  35781  fmlan0  35782  satffunlem2lem2  35797  satfv0fvfmla0  35804  satefvfmla0  35809  mrsub0  35907  mrsubccat  35909  mrsubcn  35910  elmrsubrn  35911  msubco  35922  msubvrs  35951  elmthm  35967  mthmblem  35971  ellcsrspsn  36032  elrn3  36153  dfon2lem7  36178  brsset  36278  eltrans  36280  elfix  36292  ellimits  36299  elfuns  36304  elsingles  36307  fvtransport  36423  brcolinear2  36449  fvray  36532  linedegen  36534  fvline  36535  ellines  36543  fwddifn0  36555  elhf  36565  hfninf  36577  rmoeqi  36588  rmoeqbii  36589  reueqi  36590  reueqbii  36591  rabeqbii  36595  iuneq12i  36596  iineq1i  36597  iineq12i  36598  riotaeqbii  36599  ixpeq1i  36601  itgeq12i  36607  cbvprodvw2  36648  fnessref  36757  ttctr  36893  bj-ififc  37064  bj-csbsnlem  37427  bj-elgab  37463  currysetlem1  37471  bj-eltag  37501  bj-sngltag  37507  bj-projun  37518  bj-velpwALT  37577  bj-0nelmpt  37646  bj-opelidres  37693  bj-inftyexpitaudisj  37737  bj-elccinfty  37746  f1omptsnlem  37870  icoreelrnab  37888  relowlpssretop  37898  rdgssun  37912  exrecfnlem  37913  finxpnom  37935  uncov  38140  tan2h  38151  ptrecube  38159  poimirlem25  38184  poimirlem29  38188  poimirlem30  38189  poimirlem31  38190  poimirlem32  38191  cnambfre  38207  ftc1cnnc  38231  sdclem2  38281  sdclem1  38282  fdc  38284  caushft  38300  issmgrpOLD  38402  ismndo  38411  isrngo  38436  isdivrngo  38489  csbcom2fi  38667  elecALTV  38810  brrabga  38880  eldmxrncnvepres  38973  eldmxrncnvepres2  38974  elrels2  38980  blockadjliftmap  38997  dfpre  39015  eupre  39033  eldmcoss  39087  coss0  39108  petseq  39515  dath  40400  diclspsn  41858  dvh4dimlem  42107  dvh2dim  42109  dvh3dim3N  42113  lcfrvalsnN  42205  mapdh6eN  42404  mapdh7dN  42414  mapdh8b  42444  hdmap1l6e  42478  lcmfunnnd  42669  3factsumint1  42678  primrootsunit1  42754  primrootscoprmpow  42756  aks6d1c2lem4  42784  sticksstones2  42804  sticksstones3  42805  sticksstones10  42812  sticksstones12a  42814  sticksstones12  42815  aks6d1c6lem2  42828  aks6d1c6lem3  42829  redvmptabs  43011  readvrec2  43012  readvrec  43013  frlmfielbas  43164  mhpind  43218  pellex  43454  rmspecnonsq  43526  islmodfg  43688  aaitgo  43781  areaquad  43835  ordeldif1o  43879  naddwordnexlem4  44020  fpwfvss  44030  finona1cl  44071  elcnvcnvintab  44200  elnonrel  44203  elcnvcnvlem  44217  cnvcnvintabd  44218  brfvrcld2  44310  grur1cld  44848  dvgrat  44914  cvgdvgrat  44915  radcnvrat  44916  nznngen  44918  uzmptshftfval  44948  binomcxplemcvg  44956  binomcxplemnotnn0  44958  tpid3gVD  45442  en3lplem2VD  45444  orbitclmpt  45559  wfaxrep  45595  wfaxsep  45596  wfaxpow  45598  wfaxpr  45599  wfaxun  45600  wfac8prim  45603  brpermmodelcnv  45605  nregmodellem  45617  iuneq1i  45696  rexanuz3  45706  eliuniin  45709  eliuniin2  45730  disjinfi  45802  iuneqfzuzlem  45942  allbutfi  46000  eluzelz2  46009  uz0  46018  uzublem  46036  uzid3  46041  elicores  46141  uzinico  46167  climsuselem1  46215  climsuse  46216  islptre  46227  fnlimfvre  46280  limsupresico  46306  limsupvaluz  46314  limsupubuzlem  46318  limsupequzmptlem  46334  liminfresico  46377  cnrefiisplem  46435  stoweidlem14  46620  stoweidlem39  46645  stoweidlem48  46654  stoweidlem51  46657  stoweidlem59  46665  stoweidlem62  46668  wallispilem3  46673  fourierdlem42  46755  fourierdlem62  46774  fourierdlem80  46792  fourierdlem103  46815  fourierdlem104  46816  etransclem26  46866  rrxsnicc  46906  ioorrnopn  46911  ioorrnopnxr  46913  sge00  46982  sge0fodjrnlem  47022  sge0isum  47033  sge0seq  47052  meadjiunlem  47071  carageneld  47108  volicorescl  47159  hoidmv1lelem1  47197  hoidmv1le  47200  hoidmvlelem1  47201  hoidmvlelem3  47203  ovnhoilem2  47208  hoiqssbllem2  47229  opnvonmbllem2  47239  ovolval4lem1  47255  iinhoiicc  47280  vonioolem1  47286  smflimlem1  47377  smflimlem2  47378  smflim  47383  nsssmfmbf  47385  smfresal  47394  smfrec  47395  smfdiv  47403  smfpimbor1lem2  47405  smflim2  47412  smflimmpt  47416  smfinflem  47423  smflimsuplem1  47426  smflimsuplem2  47427  smflimsuplem3  47428  smflimsuplem5  47430  smflimsuplem6  47431  smflimsup  47434  smflimsupmpt  47435  smfliminfmpt  47438  chnerlem1  47490  chnerlem2  47491  tannpoly  47516  sinnpoly  47517  fcores  47693  ndmaovcl  47829  ndmaovcom  47831  ndmaovass  47832  ndmaovdistr  47833  dfatco  47882  otiunsndisjX  47905  fvmptrabdm  47919  ceilhalfelfzo1  47960  modmknepk  47994  elsetpreimafvb  48022  sprsymrelfolem2  48131  sprsymrelf  48133  sprsymrelf1  48134  prpair  48139  prproropf1olem0  48140  paireqne  48149  fmtno4prmfac  48213  dfodd5  48314  sbgoldbo  48441  nnsum4primeseven  48454  nnsum4primesevenALTV  48455  clnbgrcl  48475  clnbgredg  48494  sclnbgrel  48501  isubgredg  48520  uhgrimedgi  48544  isuspgrim0  48548  isuspgrimlem  48549  gricushgr  48571  clnbgrgrimlem  48587  grimedg  48589  usgrgrtrirex  48604  stgrnbgr0  48618  isubgr3stgrlem3  48622  isubgr3stgrlem4  48623  isubgr3stgrlem6  48625  isubgr3stgrlem7  48626  uspgrlimlem2  48643  uspgrlimlem3  48644  grlimedgclnbgr  48649  grlimprclnbgr  48650  grlimprclnbgrvtx  48653  grlimgrtrilem2  48656  usgrexmpl2trifr  48691  gpgvtxel  48701  gpgedgel  48704  gpgusgralem  48710  gpg5order  48714  gpgvtxedg0  48717  gpgvtxedg1  48718  gpgnbgrvtx0  48728  gpgnbgrvtx1  48729  gpg5nbgrvtx03star  48734  gpg5nbgr3star  48735  gpgvtxdg3  48736  gpg5gricstgr3  48744  gpgprismgr4cycllem3  48751  gpgprismgr4cycllem7  48755  gpgprismgr4cycllem8  48756  gpgprismgr4cycllem10  48758  pgnbgreunbgrlem3  48772  pgnbgreunbgrlem6  48778  pgnbgreunbgr  48779  uspgrsprf  48800  uspgrsprf1  48801  uspgrsprfo  48802  dfidom2  48997  ply1sclrmsm  49049  lcoop  49076  lincfsuppcl  49078  linccl  49079  lincvalsng  49081  lincvalpr  49083  lincvalsc0  49086  linc0scn0  49088  lincdifsn  49089  linc1  49090  lincsum  49094  lincscm  49095  lspsslco  49102  snlindsntor  49136  lincresunit3lem2  49145  ldepsnlinclem1  49170  ldepsnlinclem2  49171  prelrrx2  49378  prelrrx2b  49379  rrx2xpref1o  49383  rrx2plord  49385  rrx2linesl  49408  sectrcl  49685  invrcl  49687  initopropdlemlem  49902  initopropd  49906  termopropd  49907  zeroopropd  49908  oppcthin  50101  indthinc  50125  prsthinc  50127  elpglem3  50376