Theorem eleq2i 2828

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811

This theorem is referenced by:  eleq12i  2829  eleqtri  2834  eleq2s  2854  hbxfreq  2866  nfceqi  2895  raleqbii  3314  rexeqbii  3315  rabeqi  3412  rabrabi  3418  reqabi  3422  elab2gw  3633  elab2g  3635  elrabf  3643  elrab3t  3645  elrab2  3649  cbvsbcw  3773  cbvsbcvw  3774  cbvsbc  3775  elin2  4155  elsymdif  4210  noel  4290  eltpg  4643  elunirab  4878  elintrab  4915  disjxiun  5095  exss  5411  otiunsndisj  5468  brabsb  5479  brabga  5482  epelg  5525  pofun  5550  elxp  5647  opeliunxp  5691  opeliun2xp  5692  bropaex12  5715  brab2a  5717  elcnv  5825  dmopabelb  5865  elrnmptg  5910  elres  5979  elimampt  6002  elrid  6005  cnv0  6097  rninxp  6137  elid  6157  elsuci  6386  elsucg  6387  elsuc2g  6388  elfv  6832  0fv  6875  opabiota  6916  dffv2  6929  fvopab3g  6936  fvmptex  6955  fvopab5  6974  fvn0ssdmfun  7019  fveqressseq  7024  f0cli  7043  fmptco  7074  fvrnressn  7106  funfvima  7176  elunirnALT  7198  fliftel  7255  eloprabga  7467  elrnmpo  7494  elimampo  7495  ovid  7499  offval  7631  1st2val  7961  2nd2val  7962  bropopvvv  8032  bropfvvvv  8034  fsplit  8059  xporderlem  8069  frpoins3xpg  8082  frpoins3xp3g  8083  brtpos2  8174  frrlem8  8235  frrlem9  8236  frrlem10  8237  fprresex  8252  issmo  8280  smores3  8285  tfrlem7  8314  tfrlem9  8316  tfrlem9a  8317  tfr2b  8327  tfr2  8329  rdgsuc  8355  frsucmptn  8370  tz7.48-2  8373  el1o  8422  ord2eln012  8424  dif1o  8427  ondif2  8429  oawordeulem  8481  elecg  8679  brecop  8747  erovlem  8750  eceqoveq  8759  mapsncnv  8831  mptelixpg  8873  brsdom  8911  isfi  8912  enssdomOLD  8914  brdom2  8919  xpcomco  8995  brsdom2  9029  en3lplem2  9522  cnfcom2lem  9610  brttrcl2  9623  ttrcltr  9625  rnttrcl  9631  epfrs  9640  r1limg  9683  r1ord  9692  r1ord3  9694  tz9.12lem3  9701  rankvaln  9711  r1elss  9718  rankpwi  9735  ssrankr1  9747  r1val3  9750  r1pw  9757  rankr1b  9776  djur  9831  djuunxp  9833  eldju2ndl  9836  eldju2ndr  9837  isnum2  9857  cardprclem  9891  infxpenlem  9923  alephcard  9980  alephnbtwn  9981  alephnbtwn2  9982  alephord2  9986  alephsdom  9996  dfac3  10031  dfac5lem2  10034  dfac5lem3  10035  dfac5lem5  10037  pwsdompw  10113  cfub  10159  cardcf  10162  cflecard  10163  cfle  10164  cflim2  10173  cofsmo  10179  cfidm  10185  isfin3  10206  isfin5  10209  isfin6  10210  sdom2en01  10212  fin23lem26  10235  fin23lem30  10252  isf32lem5  10267  itunitc1  10330  ituniiun  10332  axdc3lem3  10362  axcclem  10367  axdclem  10429  iunfo  10449  iundom2g  10450  cardidg  10458  konigthlem  10479  alephadd  10488  alephreg  10493  pwcfsdom  10494  cfpwsdom  10495  elgch  10533  fpwwe2lem11  10552  canth4  10558  wunex2  10649  r1tskina  10693  elni  10787  nlt1pi  10817  adderpq  10867  mulerpq  10868  recmulnq  10875  addsrpr  10986  mulsrpr  10987  opelcn  11040  opelreal  11041  elreal  11042  elreal2  11043  0ncn  11044  addcnsr  11046  mulcnsr  11047  xrlenlt  11197  elnn0  12403  elnnne0  12415  un0addcl  12434  un0mulcl  12435  elxnn0  12476  uztrn2  12770  elnnuz  12791  elnn0uz  12792  elq  12863  elxr  13030  elfzm1b  13518  elfz0lmr  13699  uzrdgfni  13881  fzennn  13891  ser0  13977  hash2pwpr  14399  iswrd  14438  pfxccatpfx1  14659  s3iunsndisj  14891  sumz  15645  sumss  15647  fsumcvg3  15652  abscvgcvg  15742  isumshft  15762  prodf1  15814  prodeq1i  15839  zprod  15860  prod1  15867  prodss  15870  prodsn  15885  prodsnf  15887  bpolydiflem  15977  bpoly2  15980  bpoly3  15981  bpoly4  15982  ruclem6  16160  divides  16181  dvdsflip  16244  pwp1fsum  16318  sadc0  16381  eulerthlem2  16709  prm23lt5  16742  4sqlem2  16877  4sqlem12  16884  vdwpc  16908  xpscf  17486  cidpropd  17633  oppcsect  17702  funcpropd  17826  natpropd  17903  dfinito2  17927  dftermo2  17928  initoeu2lem0  17937  arwhoma  17969  eldmcoa  17989  pospo  18266  psss  18503  ex-chn1  18560  ex-chn2  18561  ismgmn0  18567  gsumpropd2lem  18604  elefmndbas  18798  smndex1basss  18830  smndex1mgm  18832  pwmnd  18862  dfgrp2e  18893  mulgfval  18999  eqg0subg  19125  cycsubmel  19129  ghmeqker  19172  elcntr  19259  cntri  19261  cntzsgrpcl  19263  oppgsubg  19292  fvcosymgeq  19358  symgfixels  19363  pmtrfrn  19387  efgsfo  19668  efgrelexlemb  19679  lt6abl  19824  dmdprd  19929  dprdval  19934  dprdw  19941  srgbinomlem4  20164  isnirred  20356  isrhm  20414  issrng  20777  lspexchn2  21086  lspindp2l  21089  lspindp2  21090  lbsextlem2  21114  rnglidl1  21187  df2idl2  21212  2idlss  21217  rngqiprngimfo  21256  cnfldfun  21323  cnfldfunOLD  21336  pzriprnglem3  21438  pzriprnglem4  21439  pzriprnglem7  21442  pzriprnglem8  21443  pzriprnglem9  21444  pzriprnglem12  21447  pzriprnglem14  21449  dsmmelbas  21694  frlmbas3  21731  lindsind2  21774  islindf4  21793  psrbagf  21874  evlslem4  22031  psdmul  22109  ply1bascl2  22145  cply1mul  22240  lply1binom  22254  matsubgcell  22378  matinvgcell  22379  matvscacell  22380  matepmcl  22406  matepm2cl  22407  scmatscm  22457  smatvscl  22468  marrepcl  22508  marepvcl  22513  mulmarep1el  22516  mulmarep1gsum1  22517  mulmarep1gsum2  22518  submabas  22522  m1detdiag  22541  mdetdiag  22543  m2detleib  22575  gsummatr01lem3  22601  gsummatr01  22603  smadiadetlem4  22613  slesolinv  22624  slesolinvbi  22625  slesolex  22626  cramerimplem2  22628  pmatcoe1fsupp  22645  mat2pmatbas  22670  mat2pmatmul  22675  mat2pmatlin  22679  decpmatmul  22716  monmatcollpw  22723  pm2mpf1  22743  pm2mpghm  22760  istps  22878  mretopd  23036  neiptopuni  23074  lpdifsn  23087  restcls  23125  perfopn  23129  pnfnei  23164  mnfnei  23165  lmss  23242  hauscmplem  23350  is2ndc  23390  2ndcdisj  23400  hausnlly  23437  txuni2  23509  ptpjpre1  23515  elpt  23516  dfac14  23562  xkococn  23604  fbasrn  23828  fin1aufil  23876  elfm2  23892  elfm3  23894  fbflim  23920  flffbas  23939  cnpflf2  23944  fclsbas  23965  efmndtmd  24045  tsmssubm  24087  iscusp2  24245  imasdsf1olem  24317  metustel  24494  metuel2  24509  isnghm  24667  opnreen  24776  iccpnfcnv  24898  ehleudisval  25375  ehl1eudis  25376  ehl2eudis  25378  minveclem3b  25384  ovoliunlem1  25459  ioombl1lem4  25518  subopnmbl  25561  vitalilem2  25566  vitalilem3  25567  mbfimaopnlem  25612  mbfimaopn2  25614  itg2l  25686  dvply1  26247  vieta1lem1  26274  vieta1lem2  26275  elaa  26280  taylthlem2  26338  taylthlem2OLD  26339  abelthlem6  26402  abelthlem9  26406  sinq34lt0t  26474  ellogrn  26524  dvrelog  26602  ellogdm  26604  logtayl2  26627  cxpcn3lem  26713  cxpcn3  26714  1cubr  26808  atandm  26842  atanf  26846  reasinsin  26862  atans2  26897  dmarea  26923  xrlimcnp  26934  amgmlem  26956  ppiublem1  27169  lgsdir2lem2  27293  gausslemma2dlem1a  27332  lgsquadlem1  27347  lgsquadlem2  27348  2sqlem1  27384  rpvmasum2  27479  madeval2  27829  newval  27831  leftval  27845  rightval  27846  lltr  27858  madess  27862  oldssmade  27863  oldss  27866  lrold  27893  addsproplem2  27966  addsproplem4  27968  addsproplem6  27970  negsproplem4  28027  negsproplem6  28029  precsexlem10  28212  precsexlem11  28213  ltonold  28257  elnns  28336  elzs  28380  edgiedgb  29127  isuhgr  29133  isushgr  29134  isupgr  29157  isumgr  29168  umgredg  29211  umgrpredgv  29213  umgredgne  29218  umgredgnlp  29220  isuspgr  29225  isusgr  29226  ausgrusgri  29241  usgredgppr  29269  edgssv2  29271  uspgredg2vlem  29296  uspgredg2v  29297  ushgredgedg  29302  ushgredgedgloop  29304  griedg0ssusgr  29338  uhgrissubgr  29348  subumgredg2  29358  uhgrspansubgrlem  29363  umgrres1lem  29383  upgrres1  29386  nbgrcl  29408  nbuhgr  29416  nbuhgr2vtx1edgblem  29424  nbupgrres  29437  edgnbusgreu  29440  nbusgredgeu0  29441  nbusgrf1o0  29442  hashnbusgrnn0  29449  nbupgruvtxres  29480  cffldtocusgr  29520  cffldtocusgrOLD  29521  cusgrfilem2  29530  vtxdg0v  29547  vtxduhgr0nedg  29566  uhgrvd00  29608  vtxdginducedm1  29617  finsumvtxdg2ssteplem4  29622  wlk1walk  29712  wlkp1lem6  29750  iswwlks  29909  wwlknllvtx  29919  wwlksonvtx  29928  wspthnonp  29932  wlkiswwlksupgr2  29950  wwlksnwwlksnon  29988  2pthon3v  30016  umgr2wlk  30022  elwwlks2s3  30024  wwlks2onv  30026  elwwlks2ons3im  30027  isclwwlk  30059  clwwlkccatlem  30064  clwlkclwwlk  30077  wwlksext2clwwlk  30132  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  clwwlknon1  30172  clwwlknon1nloop  30174  clwwlknon2x  30178  1pthon2v  30228  uhgr3cyclex  30257  isconngr  30264  isconngr1  30265  eucrctshift  30318  frgrnbnb  30368  frgrncvvdeqlem1  30374  frgrncvvdeqlem2  30375  frgrncvvdeqlem3  30376  frgrncvvdeqlem9  30382  fusgreghash2wspv  30410  extwwlkfab  30427  numclwwlk1lem2foa  30429  numclwwlk1lem2fo  30433  clwlknon2num  30443  numclwlk2lem2f1o  30454  numclwwlk5lem  30462  topnfbey  30544  isvclem  30652  isnvlem  30685  vsfval  30708  h2hlm  31055  hhcmpl  31275  hhcms  31278  elch0  31329  omlsilem  31477  h1de2ctlem  31630  elspansni  31633  nonbooli  31726  spansncvi  31727  adjeq  32010  cnlnssadj  32155  cnvbraval  32185  brabgaf  32684  2ndresdju  32727  fmptdF  32734  fmptcof2  32735  acunirnmpt  32737  acunirnmpt2  32738  ofpreima  32743  fcnvgreu  32751  fdifsuppconst  32768  1stpreima  32786  2ndpreima  32787  fz2ssnn0  32865  elxrge02  33013  ccatws1f1o  33033  gsumwrd2dccatlem  33159  psgnfzto1stlem  33182  cycpmgcl  33235  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem4  33327  elrgspnsubrunlem1  33329  domnprodeq0  33358  nsgqusf1olem2  33495  nsgqusf1olem3  33496  prmidl0  33531  crngmxidl  33550  opprnsg  33565  rprmirredb  33613  zringfrac  33635  evl1deg2  33658  evl1deg3  33659  ply1degltel  33675  ply1degleel  33676  evlextv  33707  esplyfval3  33730  esplyindfv  33732  esplyfvn  33733  vietalem  33735  fldextrspunlsplem  33830  isconstr  33893  constrsuc  33895  constrconj  33902  submatres  33963  lmat22lem  33974  crefdf  34005  cmppcmp  34015  rspectopn  34024  prsdm  34071  prsrn  34072  xrge0iifcnv  34090  xrge0iifiso  34092  xrge0iifhom  34094  pnfneige0  34108  qqhre  34177  rrhre  34178  esumnul  34205  esumcvgsum  34245  ldgenpisyslem1  34320  measvuni  34371  cntnevol  34385  dya2iocnrect  34438  sibf0  34491  oddpwdc  34511  eulerpartlemd  34523  eulerpartgbij  34529  eulerpartlemgh  34535  isrrvv  34600  coinfliprv  34640  ballotlem7  34693  signswch  34718  hashreprin  34777  chtvalz  34786  circlemethhgt  34800  hgt750lemb  34813  tgoldbachgt  34820  bnj23  34874  bnj158  34885  bnj168  34886  bnj1138  34944  bnj1143  34946  bnj1454  34998  bnj110  35014  bnj882  35082  bnj893  35084  bnj916  35089  bnj970  35103  bnj983  35107  bnj984  35108  bnj1137  35151  bnj1174  35159  bnj1388  35189  bnj1398  35190  r1wf  35252  onvf1odlem4  35300  loop1cycl  35331  subfacp1lem5  35378  satfv1  35557  satfrnmapom  35564  satf0op  35571  satf0n0  35572  fmlafvel  35579  fmlaomn0  35584  fmlan0  35585  satffunlem2lem2  35600  satfv0fvfmla0  35607  satefvfmla0  35612  mrsub0  35710  mrsubccat  35712  mrsubcn  35713  elmrsubrn  35714  msubco  35725  msubvrs  35754  elmthm  35770  mthmblem  35774  ellcsrspsn  35835  elrn3  35956  dfon2lem7  35981  brsset  36081  eltrans  36083  elfix  36095  ellimits  36102  elfuns  36107  elsingles  36110  fvtransport  36226  brcolinear2  36252  fvray  36335  linedegen  36337  fvline  36338  ellines  36346  fwddifn0  36358  elhf  36368  hfninf  36380  rmoeqi  36381  rmoeqbii  36382  reueqi  36383  reueqbii  36384  rabeqbii  36388  iuneq12i  36389  iineq1i  36390  iineq12i  36391  riotaeqbii  36392  ixpeq1i  36394  itgeq12i  36400  cbvprodvw2  36441  fnessref  36551  bj-ififc  36782  bj-csbsnlem  37104  bj-elgab  37140  currysetlem1  37148  bj-eltag  37178  bj-sngltag  37184  bj-projun  37195  bj-velpwALT  37254  bj-0nelmpt  37321  bj-opelidres  37366  bj-inftyexpitaudisj  37410  bj-elccinfty  37419  f1omptsnlem  37541  icoreelrnab  37559  relowlpssretop  37569  rdgssun  37583  exrecfnlem  37584  finxpnom  37606  uncov  37802  tan2h  37813  ptrecube  37821  poimirlem25  37846  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  poimirlem32  37853  cnambfre  37869  ftc1cnnc  37893  sdclem2  37943  sdclem1  37944  fdc  37946  caushft  37962  issmgrpOLD  38064  ismndo  38073  isrngo  38098  isdivrngo  38151  csbcom2fi  38329  elecALTV  38464  brrabga  38534  eldmxrncnvepres  38619  eldmxrncnvepres2  38620  elrels2  38626  blockadjliftmap  38633  dfpre  38650  eupre  38667  eldmcoss  38721  coss0  38742  dath  39996  diclspsn  41454  dvh4dimlem  41703  dvh2dim  41705  dvh3dim3N  41709  lcfrvalsnN  41801  mapdh6eN  42000  mapdh7dN  42010  mapdh8b  42040  hdmap1l6e  42074  lcmfunnnd  42266  3factsumint1  42275  primrootsunit1  42351  primrootscoprmpow  42353  aks6d1c2lem4  42381  sticksstones2  42401  sticksstones3  42402  sticksstones10  42409  sticksstones12a  42411  sticksstones12  42412  aks6d1c6lem2  42425  aks6d1c6lem3  42426  redvmptabs  42615  readvrec2  42616  readvrec  42617  frlmfielbas  42755  mhpind  42837  pellex  43077  rmspecnonsq  43149  islmodfg  43311  aaitgo  43404  areaquad  43458  ordeldif1o  43502  naddwordnexlem4  43643  fpwfvss  43653  finona1cl  43694  elcnvcnvintab  43823  elnonrel  43826  elcnvcnvlem  43840  cnvcnvintabd  43841  brfvrcld2  43933  grur1cld  44473  dvgrat  44553  cvgdvgrat  44554  radcnvrat  44555  nznngen  44557  uzmptshftfval  44587  binomcxplemcvg  44595  binomcxplemnotnn0  44597  tpid3gVD  45082  en3lplem2VD  45084  orbitclmpt  45199  wfaxrep  45235  wfaxsep  45236  wfaxpow  45238  wfaxpr  45239  wfaxun  45240  wfac8prim  45243  brpermmodelcnv  45245  nregmodellem  45257  iuneq1i  45329  rexanuz3  45340  eliuniin  45343  eliuniin2  45364  disjinfi  45436  fsneq  45450  iuneqfzuzlem  45579  allbutfi  45637  eluzelz2  45647  uz0  45656  uzublem  45674  uzid3  45679  elicores  45779  uzinico  45805  climsuselem1  45853  climsuse  45854  islptre  45865  fnlimfvre  45918  limsupresico  45944  limsupvaluz  45952  limsupubuzlem  45956  limsupequzmptlem  45972  liminfresico  46015  cnrefiisplem  46073  stoweidlem14  46258  stoweidlem39  46283  stoweidlem48  46292  stoweidlem51  46295  stoweidlem59  46303  stoweidlem62  46306  wallispilem3  46311  fourierdlem42  46393  fourierdlem62  46412  fourierdlem80  46430  fourierdlem103  46453  fourierdlem104  46454  etransclem26  46504  rrxsnicc  46544  ioorrnopn  46549  ioorrnopnxr  46551  sge00  46620  sge0fodjrnlem  46660  sge0isum  46671  sge0seq  46690  meadjiunlem  46709  carageneld  46746  volicorescl  46797  hoidmv1lelem1  46835  hoidmv1le  46838  hoidmvlelem1  46839  hoidmvlelem3  46841  ovnhoilem2  46846  hoiqssbllem2  46867  opnvonmbllem2  46877  ovolval4lem1  46893  iinhoiicc  46918  vonioolem1  46924  smflimlem1  47015  smflimlem2  47016  smflim  47021  nsssmfmbf  47023  smfresal  47032  smfrec  47033  smfdiv  47041  smfpimbor1lem2  47043  smflim2  47050  smflimmpt  47054  smfinflem  47061  smflimsuplem1  47064  smflimsuplem2  47065  smflimsuplem3  47066  smflimsuplem5  47068  smflimsuplem6  47069  smflimsup  47072  smflimsupmpt  47073  smfliminfmpt  47076  chnerlem1  47126  chnerlem2  47127  tannpoly  47136  sinnpoly  47137  fcores  47313  ndmaovcl  47449  ndmaovcom  47451  ndmaovass  47452  ndmaovdistr  47453  dfatco  47502  otiunsndisjX  47525  fvmptrabdm  47539  ceilhalfelfzo1  47576  modmknepk  47608  elsetpreimafvb  47630  sprsymrelfolem2  47739  sprsymrelf  47741  sprsymrelf1  47742  prpair  47747  prproropf1olem0  47748  paireqne  47757  fmtno4prmfac  47818  dfodd5  47906  sbgoldbo  48033  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  clnbgrcl  48067  clnbgredg  48086  sclnbgrel  48093  isubgredg  48112  uhgrimedgi  48136  isuspgrim0  48140  isuspgrimlem  48141  gricushgr  48163  clnbgrgrimlem  48179  grimedg  48181  usgrgrtrirex  48196  stgrnbgr0  48210  isubgr3stgrlem3  48214  isubgr3stgrlem4  48215  isubgr3stgrlem6  48217  isubgr3stgrlem7  48218  uspgrlimlem2  48235  uspgrlimlem3  48236  grlimedgclnbgr  48241  grlimprclnbgr  48242  grlimprclnbgrvtx  48245  grlimgrtrilem2  48248  usgrexmpl2trifr  48283  gpgvtxel  48293  gpgedgel  48296  gpgusgralem  48302  gpg5order  48306  gpgvtxedg0  48309  gpgvtxedg1  48310  gpgnbgrvtx0  48320  gpgnbgrvtx1  48321  gpg5nbgrvtx03star  48326  gpg5nbgr3star  48327  gpgvtxdg3  48328  gpg5gricstgr3  48336  gpgprismgr4cycllem3  48343  gpgprismgr4cycllem7  48347  gpgprismgr4cycllem8  48348  gpgprismgr4cycllem10  48350  pgnbgreunbgrlem3  48364  pgnbgreunbgrlem6  48370  pgnbgreunbgr  48371  uspgrsprf  48392  uspgrsprf1  48393  uspgrsprfo  48394  ply1sclrmsm  48630  lcoop  48657  lincfsuppcl  48659  linccl  48660  lincvalsng  48662  lincvalpr  48664  lincvalsc0  48667  linc0scn0  48669  lincdifsn  48670  linc1  48671  lincsum  48675  lincscm  48676  lspsslco  48683  snlindsntor  48717  lincresunit3lem2  48726  ldepsnlinclem1  48751  ldepsnlinclem2  48752  prelrrx2  48959  prelrrx2b  48960  rrx2xpref1o  48964  rrx2plord  48966  rrx2linesl  48989  sectrcl  49267  invrcl  49269  initopropdlemlem  49484  initopropd  49488  termopropd  49489  zeroopropd  49490  oppcthin  49683  indthinc  49707  prsthinc  49709  elpglem3  49958