Theorem eleq2i 2829

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eleq12i  2830  eleqtri  2835  eleq2s  2855  hbxfreq  2867  nfceqi  2896  raleqbii  3316  rexeqbii  3317  rabeqi  3414  rabrabi  3420  reqabi  3424  elab2gw  3635  elab2g  3637  elrabf  3645  elrab3t  3647  elrab2  3651  cbvsbcw  3775  cbvsbcvw  3776  cbvsbc  3777  elin2  4157  elsymdif  4212  noel  4292  eltpg  4645  elunirab  4880  elintrab  4917  disjxiun  5097  exss  5418  otiunsndisj  5476  brabsb  5487  brabga  5490  epelg  5533  pofun  5558  elxp  5655  opeliunxp  5699  opeliun2xp  5700  bropaex12  5723  brab2a  5725  elcnv  5833  dmopabelb  5873  elrnmptg  5918  elres  5987  elimampt  6010  elrid  6013  cnv0  6105  rninxp  6145  elid  6165  elsuci  6394  elsucg  6395  elsuc2g  6396  elfv  6840  0fv  6883  opabiota  6924  dffv2  6937  fvopab3g  6944  fvmptex  6964  fvopab5  6983  fvn0ssdmfun  7028  fveqressseq  7033  f0cli  7052  fmptco  7084  fvrnressn  7116  funfvima  7186  elunirnALT  7208  fliftel  7265  eloprabga  7477  elrnmpo  7504  elimampo  7505  ovid  7509  offval  7641  1st2val  7971  2nd2val  7972  bropopvvv  8042  bropfvvvv  8044  fsplit  8069  xporderlem  8079  frpoins3xpg  8092  frpoins3xp3g  8093  brtpos2  8184  frrlem8  8245  frrlem9  8246  frrlem10  8247  fprresex  8262  issmo  8290  smores3  8295  tfrlem7  8324  tfrlem9  8326  tfrlem9a  8327  tfr2b  8337  tfr2  8339  rdgsuc  8365  frsucmptn  8380  tz7.48-2  8383  el1o  8432  ord2eln012  8434  dif1o  8437  ondif2  8439  oawordeulem  8491  elecg  8690  brecop  8759  erovlem  8762  eceqoveq  8771  mapsncnv  8843  mptelixpg  8885  brsdom  8923  isfi  8924  enssdomOLD  8926  brdom2  8931  xpcomco  9007  brsdom2  9041  en3lplem2  9534  cnfcom2lem  9622  brttrcl2  9635  ttrcltr  9637  rnttrcl  9643  epfrs  9652  r1limg  9695  r1ord  9704  r1ord3  9706  tz9.12lem3  9713  rankvaln  9723  r1elss  9730  rankpwi  9747  ssrankr1  9759  r1val3  9762  r1pw  9769  rankr1b  9788  djur  9843  djuunxp  9845  eldju2ndl  9848  eldju2ndr  9849  isnum2  9869  cardprclem  9903  infxpenlem  9935  alephcard  9992  alephnbtwn  9993  alephnbtwn2  9994  alephord2  9998  alephsdom  10008  dfac3  10043  dfac5lem2  10046  dfac5lem3  10047  dfac5lem5  10049  pwsdompw  10125  cfub  10171  cardcf  10174  cflecard  10175  cfle  10176  cflim2  10185  cofsmo  10191  cfidm  10197  isfin3  10218  isfin5  10221  isfin6  10222  sdom2en01  10224  fin23lem26  10247  fin23lem30  10264  isf32lem5  10279  itunitc1  10342  ituniiun  10344  axdc3lem3  10374  axcclem  10379  axdclem  10441  iunfo  10461  iundom2g  10462  cardidg  10470  konigthlem  10491  alephadd  10500  alephreg  10505  pwcfsdom  10506  cfpwsdom  10507  elgch  10545  fpwwe2lem11  10564  canth4  10570  wunex2  10661  r1tskina  10705  elni  10799  nlt1pi  10829  adderpq  10879  mulerpq  10880  recmulnq  10887  addsrpr  10998  mulsrpr  10999  opelcn  11052  opelreal  11053  elreal  11054  elreal2  11055  0ncn  11056  addcnsr  11058  mulcnsr  11059  xrlenlt  11209  elnn0  12415  elnnne0  12427  un0addcl  12446  un0mulcl  12447  elxnn0  12488  uztrn2  12782  elnnuz  12803  elnn0uz  12804  elq  12875  elxr  13042  elfzm1b  13530  elfz0lmr  13711  uzrdgfni  13893  fzennn  13903  ser0  13989  hash2pwpr  14411  iswrd  14450  pfxccatpfx1  14671  s3iunsndisj  14903  sumz  15657  sumss  15659  fsumcvg3  15664  abscvgcvg  15754  isumshft  15774  prodf1  15826  prodeq1i  15851  zprod  15872  prod1  15879  prodss  15882  prodsn  15897  prodsnf  15899  bpolydiflem  15989  bpoly2  15992  bpoly3  15993  bpoly4  15994  ruclem6  16172  divides  16193  dvdsflip  16256  pwp1fsum  16330  sadc0  16393  eulerthlem2  16721  prm23lt5  16754  4sqlem2  16889  4sqlem12  16896  vdwpc  16920  xpscf  17498  cidpropd  17645  oppcsect  17714  funcpropd  17838  natpropd  17915  dfinito2  17939  dftermo2  17940  initoeu2lem0  17949  arwhoma  17981  eldmcoa  18001  pospo  18278  psss  18515  ex-chn1  18572  ex-chn2  18573  ismgmn0  18579  gsumpropd2lem  18616  elefmndbas  18810  smndex1basss  18842  smndex1mgm  18844  pwmnd  18874  dfgrp2e  18905  mulgfval  19011  eqg0subg  19137  cycsubmel  19141  ghmeqker  19184  elcntr  19271  cntri  19273  cntzsgrpcl  19275  oppgsubg  19304  fvcosymgeq  19370  symgfixels  19375  pmtrfrn  19399  efgsfo  19680  efgrelexlemb  19691  lt6abl  19836  dmdprd  19941  dprdval  19946  dprdw  19953  srgbinomlem4  20176  isnirred  20368  isrhm  20426  issrng  20789  lspexchn2  21098  lspindp2l  21101  lspindp2  21102  lbsextlem2  21126  rnglidl1  21199  df2idl2  21224  2idlss  21229  rngqiprngimfo  21268  cnfldfun  21335  cnfldfunOLD  21348  pzriprnglem3  21450  pzriprnglem4  21451  pzriprnglem7  21454  pzriprnglem8  21455  pzriprnglem9  21456  pzriprnglem12  21459  pzriprnglem14  21461  dsmmelbas  21706  frlmbas3  21743  lindsind2  21786  islindf4  21805  psrbagf  21886  evlslem4  22043  psdmul  22121  ply1bascl2  22157  cply1mul  22252  lply1binom  22266  matsubgcell  22390  matinvgcell  22391  matvscacell  22392  matepmcl  22418  matepm2cl  22419  scmatscm  22469  smatvscl  22480  marrepcl  22520  marepvcl  22525  mulmarep1el  22528  mulmarep1gsum1  22529  mulmarep1gsum2  22530  submabas  22534  m1detdiag  22553  mdetdiag  22555  m2detleib  22587  gsummatr01lem3  22613  gsummatr01  22615  smadiadetlem4  22625  slesolinv  22636  slesolinvbi  22637  slesolex  22638  cramerimplem2  22640  pmatcoe1fsupp  22657  mat2pmatbas  22682  mat2pmatmul  22687  mat2pmatlin  22691  decpmatmul  22728  monmatcollpw  22735  pm2mpf1  22755  pm2mpghm  22772  istps  22890  mretopd  23048  neiptopuni  23086  lpdifsn  23099  restcls  23137  perfopn  23141  pnfnei  23176  mnfnei  23177  lmss  23254  hauscmplem  23362  is2ndc  23402  2ndcdisj  23412  hausnlly  23449  txuni2  23521  ptpjpre1  23527  elpt  23528  dfac14  23574  xkococn  23616  fbasrn  23840  fin1aufil  23888  elfm2  23904  elfm3  23906  fbflim  23932  flffbas  23951  cnpflf2  23956  fclsbas  23977  efmndtmd  24057  tsmssubm  24099  iscusp2  24257  imasdsf1olem  24329  metustel  24506  metuel2  24521  isnghm  24679  opnreen  24788  iccpnfcnv  24910  ehleudisval  25387  ehl1eudis  25388  ehl2eudis  25390  minveclem3b  25396  ovoliunlem1  25471  ioombl1lem4  25530  subopnmbl  25573  vitalilem2  25578  vitalilem3  25579  mbfimaopnlem  25624  mbfimaopn2  25626  itg2l  25698  dvply1  26259  vieta1lem1  26286  vieta1lem2  26287  elaa  26292  taylthlem2  26350  taylthlem2OLD  26351  abelthlem6  26414  abelthlem9  26418  sinq34lt0t  26486  ellogrn  26536  dvrelog  26614  ellogdm  26616  logtayl2  26639  cxpcn3lem  26725  cxpcn3  26726  1cubr  26820  atandm  26854  atanf  26858  reasinsin  26874  atans2  26909  dmarea  26935  xrlimcnp  26946  amgmlem  26968  ppiublem1  27181  lgsdir2lem2  27305  gausslemma2dlem1a  27344  lgsquadlem1  27359  lgsquadlem2  27360  2sqlem1  27396  rpvmasum2  27491  madeval2  27841  newval  27843  leftval  27857  rightval  27858  lltr  27870  madess  27874  oldssmade  27875  oldss  27878  lrold  27905  addsproplem2  27978  addsproplem4  27980  addsproplem6  27982  negsproplem4  28039  negsproplem6  28041  precsexlem10  28224  precsexlem11  28225  ltonold  28269  elnns  28348  elzs  28392  edgiedgb  29139  isuhgr  29145  isushgr  29146  isupgr  29169  isumgr  29180  umgredg  29223  umgrpredgv  29225  umgredgne  29230  umgredgnlp  29232  isuspgr  29237  isusgr  29238  ausgrusgri  29253  usgredgppr  29281  edgssv2  29283  uspgredg2vlem  29308  uspgredg2v  29309  ushgredgedg  29314  ushgredgedgloop  29316  griedg0ssusgr  29350  uhgrissubgr  29360  subumgredg2  29370  uhgrspansubgrlem  29375  umgrres1lem  29395  upgrres1  29398  nbgrcl  29420  nbuhgr  29428  nbuhgr2vtx1edgblem  29436  nbupgrres  29449  edgnbusgreu  29452  nbusgredgeu0  29453  nbusgrf1o0  29454  hashnbusgrnn0  29461  nbupgruvtxres  29492  cffldtocusgr  29532  cffldtocusgrOLD  29533  cusgrfilem2  29542  vtxdg0v  29559  vtxduhgr0nedg  29578  uhgrvd00  29620  vtxdginducedm1  29629  finsumvtxdg2ssteplem4  29634  wlk1walk  29724  wlkp1lem6  29762  iswwlks  29921  wwlknllvtx  29931  wwlksonvtx  29940  wspthnonp  29944  wlkiswwlksupgr2  29962  wwlksnwwlksnon  30000  2pthon3v  30028  umgr2wlk  30034  elwwlks2s3  30036  wwlks2onv  30038  elwwlks2ons3im  30039  isclwwlk  30071  clwwlkccatlem  30076  clwlkclwwlk  30089  wwlksext2clwwlk  30144  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  clwwlknon1  30184  clwwlknon1nloop  30186  clwwlknon2x  30190  1pthon2v  30240  uhgr3cyclex  30269  isconngr  30276  isconngr1  30277  eucrctshift  30330  frgrnbnb  30380  frgrncvvdeqlem1  30386  frgrncvvdeqlem2  30387  frgrncvvdeqlem3  30388  frgrncvvdeqlem9  30394  fusgreghash2wspv  30422  extwwlkfab  30439  numclwwlk1lem2foa  30441  numclwwlk1lem2fo  30445  clwlknon2num  30455  numclwlk2lem2f1o  30466  numclwwlk5lem  30474  topnfbey  30556  isvclem  30665  isnvlem  30698  vsfval  30721  h2hlm  31068  hhcmpl  31288  hhcms  31291  elch0  31342  omlsilem  31490  h1de2ctlem  31643  elspansni  31646  nonbooli  31739  spansncvi  31740  adjeq  32023  cnlnssadj  32168  cnvbraval  32198  brabgaf  32696  2ndresdju  32739  fmptdF  32746  fmptcof2  32747  acunirnmpt  32749  acunirnmpt2  32750  ofpreima  32755  fcnvgreu  32762  fdifsuppconst  32779  1stpreima  32797  2ndpreima  32798  fz2ssnn0  32876  elxrge02  33024  ccatws1f1o  33044  gsumwrd2dccatlem  33171  psgnfzto1stlem  33194  cycpmgcl  33247  elrgspnlem1  33336  elrgspnlem2  33337  elrgspnlem4  33339  elrgspnsubrunlem1  33341  domnprodeq0  33370  nsgqusf1olem2  33507  nsgqusf1olem3  33508  prmidl0  33543  crngmxidl  33562  opprnsg  33577  rprmirredb  33625  zringfrac  33647  evl1deg2  33670  evl1deg3  33671  ply1degltel  33687  ply1degleel  33688  evlextv  33719  esplyfval3  33749  esplyindfv  33753  esplyfvn  33754  vietalem  33756  fldextrspunlsplem  33851  isconstr  33914  constrsuc  33916  constrconj  33923  submatres  33984  lmat22lem  33995  crefdf  34026  cmppcmp  34036  rspectopn  34045  prsdm  34092  prsrn  34093  xrge0iifcnv  34111  xrge0iifiso  34113  xrge0iifhom  34115  pnfneige0  34129  qqhre  34198  rrhre  34199  esumnul  34226  esumcvgsum  34266  ldgenpisyslem1  34341  measvuni  34392  cntnevol  34406  dya2iocnrect  34459  sibf0  34512  oddpwdc  34532  eulerpartlemd  34544  eulerpartgbij  34550  eulerpartlemgh  34556  isrrvv  34621  coinfliprv  34661  ballotlem7  34714  signswch  34739  hashreprin  34798  chtvalz  34807  circlemethhgt  34821  hgt750lemb  34834  tgoldbachgt  34841  bnj23  34895  bnj158  34906  bnj168  34907  bnj1138  34965  bnj1143  34966  bnj1454  35018  bnj110  35034  bnj882  35102  bnj893  35104  bnj916  35109  bnj970  35123  bnj983  35127  bnj984  35128  bnj1137  35171  bnj1174  35179  bnj1388  35209  bnj1398  35210  r1wf  35273  onvf1odlem4  35322  loop1cycl  35353  subfacp1lem5  35400  satfv1  35579  satfrnmapom  35586  satf0op  35593  satf0n0  35594  fmlafvel  35601  fmlaomn0  35606  fmlan0  35607  satffunlem2lem2  35622  satfv0fvfmla0  35629  satefvfmla0  35634  mrsub0  35732  mrsubccat  35734  mrsubcn  35735  elmrsubrn  35736  msubco  35747  msubvrs  35776  elmthm  35792  mthmblem  35796  ellcsrspsn  35857  elrn3  35978  dfon2lem7  36003  brsset  36103  eltrans  36105  elfix  36117  ellimits  36124  elfuns  36129  elsingles  36132  fvtransport  36248  brcolinear2  36274  fvray  36357  linedegen  36359  fvline  36360  ellines  36368  fwddifn0  36380  elhf  36390  hfninf  36402  rmoeqi  36403  rmoeqbii  36404  reueqi  36405  reueqbii  36406  rabeqbii  36410  iuneq12i  36411  iineq1i  36412  iineq12i  36413  riotaeqbii  36414  ixpeq1i  36416  itgeq12i  36422  cbvprodvw2  36463  fnessref  36573  bj-ififc  36807  bj-csbsnlem  37151  bj-elgab  37187  currysetlem1  37195  bj-eltag  37225  bj-sngltag  37231  bj-projun  37242  bj-velpwALT  37301  bj-0nelmpt  37369  bj-opelidres  37416  bj-inftyexpitaudisj  37460  bj-elccinfty  37469  f1omptsnlem  37591  icoreelrnab  37609  relowlpssretop  37619  rdgssun  37633  exrecfnlem  37634  finxpnom  37656  uncov  37852  tan2h  37863  ptrecube  37871  poimirlem25  37896  poimirlem29  37900  poimirlem30  37901  poimirlem31  37902  poimirlem32  37903  cnambfre  37919  ftc1cnnc  37943  sdclem2  37993  sdclem1  37994  fdc  37996  caushft  38012  issmgrpOLD  38114  ismndo  38123  isrngo  38148  isdivrngo  38201  csbcom2fi  38379  elecALTV  38522  brrabga  38592  eldmxrncnvepres  38685  eldmxrncnvepres2  38686  elrels2  38692  blockadjliftmap  38709  dfpre  38727  eupre  38745  eldmcoss  38799  coss0  38820  petseq  39227  dath  40112  diclspsn  41570  dvh4dimlem  41819  dvh2dim  41821  dvh3dim3N  41825  lcfrvalsnN  41917  mapdh6eN  42116  mapdh7dN  42126  mapdh8b  42156  hdmap1l6e  42190  lcmfunnnd  42382  3factsumint1  42391  primrootsunit1  42467  primrootscoprmpow  42469  aks6d1c2lem4  42497  sticksstones2  42517  sticksstones3  42518  sticksstones10  42525  sticksstones12a  42527  sticksstones12  42528  aks6d1c6lem2  42541  aks6d1c6lem3  42542  redvmptabs  42730  readvrec2  42731  readvrec  42732  frlmfielbas  42870  mhpind  42952  pellex  43192  rmspecnonsq  43264  islmodfg  43426  aaitgo  43519  areaquad  43573  ordeldif1o  43617  naddwordnexlem4  43758  fpwfvss  43768  finona1cl  43809  elcnvcnvintab  43938  elnonrel  43941  elcnvcnvlem  43955  cnvcnvintabd  43956  brfvrcld2  44048  grur1cld  44588  dvgrat  44668  cvgdvgrat  44669  radcnvrat  44670  nznngen  44672  uzmptshftfval  44702  binomcxplemcvg  44710  binomcxplemnotnn0  44712  tpid3gVD  45197  en3lplem2VD  45199  orbitclmpt  45314  wfaxrep  45350  wfaxsep  45351  wfaxpow  45353  wfaxpr  45354  wfaxun  45355  wfac8prim  45358  brpermmodelcnv  45360  nregmodellem  45372  iuneq1i  45444  rexanuz3  45455  eliuniin  45458  eliuniin2  45479  disjinfi  45551  fsneq  45564  iuneqfzuzlem  45693  allbutfi  45751  eluzelz2  45761  uz0  45770  uzublem  45788  uzid3  45793  elicores  45893  uzinico  45919  climsuselem1  45967  climsuse  45968  islptre  45979  fnlimfvre  46032  limsupresico  46058  limsupvaluz  46066  limsupubuzlem  46070  limsupequzmptlem  46086  liminfresico  46129  cnrefiisplem  46187  stoweidlem14  46372  stoweidlem39  46397  stoweidlem48  46406  stoweidlem51  46409  stoweidlem59  46417  stoweidlem62  46420  wallispilem3  46425  fourierdlem42  46507  fourierdlem62  46526  fourierdlem80  46544  fourierdlem103  46567  fourierdlem104  46568  etransclem26  46618  rrxsnicc  46658  ioorrnopn  46663  ioorrnopnxr  46665  sge00  46734  sge0fodjrnlem  46774  sge0isum  46785  sge0seq  46804  meadjiunlem  46823  carageneld  46860  volicorescl  46911  hoidmv1lelem1  46949  hoidmv1le  46952  hoidmvlelem1  46953  hoidmvlelem3  46955  ovnhoilem2  46960  hoiqssbllem2  46981  opnvonmbllem2  46991  ovolval4lem1  47007  iinhoiicc  47032  vonioolem1  47038  smflimlem1  47129  smflimlem2  47130  smflim  47135  nsssmfmbf  47137  smfresal  47146  smfrec  47147  smfdiv  47155  smfpimbor1lem2  47157  smflim2  47164  smflimmpt  47168  smfinflem  47175  smflimsuplem1  47178  smflimsuplem2  47179  smflimsuplem3  47180  smflimsuplem5  47182  smflimsuplem6  47183  smflimsup  47186  smflimsupmpt  47187  smfliminfmpt  47190  chnerlem1  47240  chnerlem2  47241  tannpoly  47250  sinnpoly  47251  fcores  47427  ndmaovcl  47563  ndmaovcom  47565  ndmaovass  47566  ndmaovdistr  47567  dfatco  47616  otiunsndisjX  47639  fvmptrabdm  47653  ceilhalfelfzo1  47690  modmknepk  47722  elsetpreimafvb  47744  sprsymrelfolem2  47853  sprsymrelf  47855  sprsymrelf1  47856  prpair  47861  prproropf1olem0  47862  paireqne  47871  fmtno4prmfac  47932  dfodd5  48020  sbgoldbo  48147  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  clnbgrcl  48181  clnbgredg  48200  sclnbgrel  48207  isubgredg  48226  uhgrimedgi  48250  isuspgrim0  48254  isuspgrimlem  48255  gricushgr  48277  clnbgrgrimlem  48293  grimedg  48295  usgrgrtrirex  48310  stgrnbgr0  48324  isubgr3stgrlem3  48328  isubgr3stgrlem4  48329  isubgr3stgrlem6  48331  isubgr3stgrlem7  48332  uspgrlimlem2  48349  uspgrlimlem3  48350  grlimedgclnbgr  48355  grlimprclnbgr  48356  grlimprclnbgrvtx  48359  grlimgrtrilem2  48362  usgrexmpl2trifr  48397  gpgvtxel  48407  gpgedgel  48410  gpgusgralem  48416  gpg5order  48420  gpgvtxedg0  48423  gpgvtxedg1  48424  gpgnbgrvtx0  48434  gpgnbgrvtx1  48435  gpg5nbgrvtx03star  48440  gpg5nbgr3star  48441  gpgvtxdg3  48442  gpg5gricstgr3  48450  gpgprismgr4cycllem3  48457  gpgprismgr4cycllem7  48461  gpgprismgr4cycllem8  48462  gpgprismgr4cycllem10  48464  pgnbgreunbgrlem3  48478  pgnbgreunbgrlem6  48484  pgnbgreunbgr  48485  uspgrsprf  48506  uspgrsprf1  48507  uspgrsprfo  48508  ply1sclrmsm  48744  lcoop  48771  lincfsuppcl  48773  linccl  48774  lincvalsng  48776  lincvalpr  48778  lincvalsc0  48781  linc0scn0  48783  lincdifsn  48784  linc1  48785  lincsum  48789  lincscm  48790  lspsslco  48797  snlindsntor  48831  lincresunit3lem2  48840  ldepsnlinclem1  48865  ldepsnlinclem2  48866  prelrrx2  49073  prelrrx2b  49074  rrx2xpref1o  49078  rrx2plord  49080  rrx2linesl  49103  sectrcl  49381  invrcl  49383  initopropdlemlem  49598  initopropd  49602  termopropd  49603  zeroopropd  49604  oppcthin  49797  indthinc  49821  prsthinc  49823  elpglem3  50072