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  3310  rexeqbii  3311  rabeqi  3403  rabrabi  3409  reqabi  3413  elab2gw  3622  elab2g  3624  elrabf  3632  elrab3t  3634  elrab2  3638  cbvsbcw  3762  cbvsbcvw  3763  cbvsbc  3764  elin2  4144  elsymdif  4199  noel  4279  eltpg  4631  elunirab  4866  elintrab  4903  disjxiun  5083  exss  5411  otiunsndisj  5469  brabsb  5480  brabga  5483  epelg  5526  pofun  5551  elxp  5648  opeliunxp  5692  opeliun2xp  5693  bropaex12  5716  brab2a  5718  elcnv  5826  dmopabelb  5866  elrnmptg  5911  elres  5980  elimampt  6003  elrid  6006  cnv0  6098  rninxp  6138  elid  6158  elsuci  6387  elsucg  6388  elsuc2g  6389  elfv  6833  0fv  6876  opabiota  6917  dffv2  6930  fvopab3g  6937  fvmptex  6957  fvopab5  6976  fvn0ssdmfun  7021  fveqressseq  7026  f0cli  7045  fmptco  7077  fvrnressn  7109  funfvima  7179  elunirnALT  7201  fliftel  7258  eloprabga  7470  elrnmpo  7497  elimampo  7498  ovid  7502  offval  7634  1st2val  7964  2nd2val  7965  bropopvvv  8034  bropfvvvv  8036  fsplit  8061  xporderlem  8071  frpoins3xpg  8084  frpoins3xp3g  8085  brtpos2  8176  frrlem8  8237  frrlem9  8238  frrlem10  8239  fprresex  8254  issmo  8282  smores3  8287  tfrlem7  8316  tfrlem9  8318  tfrlem9a  8319  tfr2b  8329  tfr2  8331  rdgsuc  8357  frsucmptn  8372  tz7.48-2  8375  el1o  8424  ord2eln012  8426  dif1o  8429  ondif2  8431  oawordeulem  8483  elecg  8682  brecop  8751  erovlem  8754  eceqoveq  8763  mapsncnv  8835  mptelixpg  8877  brsdom  8915  isfi  8916  enssdomOLD  8918  brdom2  8923  xpcomco  8999  brsdom2  9033  en3lplem2  9528  cnfcom2lem  9616  brttrcl2  9629  ttrcltr  9631  rnttrcl  9637  epfrs  9646  r1limg  9689  r1ord  9698  r1ord3  9700  tz9.12lem3  9707  rankvaln  9717  r1elss  9724  rankpwi  9741  ssrankr1  9753  r1val3  9756  r1pw  9763  rankr1b  9782  djur  9837  djuunxp  9839  eldju2ndl  9842  eldju2ndr  9843  isnum2  9863  cardprclem  9897  infxpenlem  9929  alephcard  9986  alephnbtwn  9987  alephnbtwn2  9988  alephord2  9992  alephsdom  10002  dfac3  10037  dfac5lem2  10040  dfac5lem3  10041  dfac5lem5  10043  pwsdompw  10119  cfub  10165  cardcf  10168  cflecard  10169  cfle  10170  cflim2  10179  cofsmo  10185  cfidm  10191  isfin3  10212  isfin5  10215  isfin6  10216  sdom2en01  10218  fin23lem26  10241  fin23lem30  10258  isf32lem5  10273  itunitc1  10336  ituniiun  10338  axdc3lem3  10368  axcclem  10373  axdclem  10435  iunfo  10455  iundom2g  10456  cardidg  10464  konigthlem  10485  alephadd  10494  alephreg  10499  pwcfsdom  10500  cfpwsdom  10501  elgch  10539  fpwwe2lem11  10558  canth4  10564  wunex2  10655  r1tskina  10699  elni  10793  nlt1pi  10823  adderpq  10873  mulerpq  10874  recmulnq  10881  addsrpr  10992  mulsrpr  10993  opelcn  11046  opelreal  11047  elreal  11048  elreal2  11049  0ncn  11050  addcnsr  11052  mulcnsr  11053  xrlenlt  11204  elnn0  12433  elnnne0  12445  un0addcl  12464  un0mulcl  12465  elxnn0  12506  uztrn2  12801  elnnuz  12822  elnn0uz  12823  elq  12894  elxr  13061  elfzm1b  13550  elfz0lmr  13732  uzrdgfni  13914  fzennn  13924  ser0  14010  hash2pwpr  14432  iswrd  14471  pfxccatpfx1  14692  s3iunsndisj  14924  sumz  15678  sumss  15680  fsumcvg3  15685  abscvgcvg  15776  isumshft  15798  prodf1  15850  prodeq1i  15875  zprod  15896  prod1  15903  prodss  15906  prodsn  15921  prodsnf  15923  bpolydiflem  16013  bpoly2  16016  bpoly3  16017  bpoly4  16018  ruclem6  16196  divides  16217  dvdsflip  16280  pwp1fsum  16354  sadc0  16417  eulerthlem2  16746  prm23lt5  16779  4sqlem2  16914  4sqlem12  16921  vdwpc  16945  xpscf  17523  cidpropd  17670  oppcsect  17739  funcpropd  17863  natpropd  17940  dfinito2  17964  dftermo2  17965  initoeu2lem0  17974  arwhoma  18006  eldmcoa  18026  pospo  18303  psss  18540  ex-chn1  18597  ex-chn2  18598  ismgmn0  18604  gsumpropd2lem  18641  elefmndbas  18835  smndex1basss  18870  smndex1mgm  18872  pwmnd  18902  dfgrp2e  18933  mulgfval  19039  eqg0subg  19165  cycsubmel  19169  ghmeqker  19212  elcntr  19299  cntri  19301  cntzsgrpcl  19303  oppgsubg  19332  fvcosymgeq  19398  symgfixels  19403  pmtrfrn  19427  efgsfo  19708  efgrelexlemb  19719  lt6abl  19864  dmdprd  19969  dprdval  19974  dprdw  19981  srgbinomlem4  20204  isnirred  20394  isrhm  20452  issrng  20815  lspexchn2  21124  lspindp2l  21127  lspindp2  21128  lbsextlem2  21152  rnglidl1  21225  df2idl2  21250  2idlss  21255  rngqiprngimfo  21294  cnfldfun  21361  cnfldfunOLD  21374  pzriprnglem3  21476  pzriprnglem4  21477  pzriprnglem7  21480  pzriprnglem8  21481  pzriprnglem9  21482  pzriprnglem12  21485  pzriprnglem14  21487  dsmmelbas  21732  frlmbas3  21769  lindsind2  21812  islindf4  21831  psrbagf  21911  evlslem4  22067  psdmul  22145  ply1bascl2  22181  cply1mul  22274  lply1binom  22288  matsubgcell  22412  matinvgcell  22413  matvscacell  22414  matepmcl  22440  matepm2cl  22441  scmatscm  22491  smatvscl  22502  marrepcl  22542  marepvcl  22547  mulmarep1el  22550  mulmarep1gsum1  22551  mulmarep1gsum2  22552  submabas  22556  m1detdiag  22575  mdetdiag  22577  m2detleib  22609  gsummatr01lem3  22635  gsummatr01  22637  smadiadetlem4  22647  slesolinv  22658  slesolinvbi  22659  slesolex  22660  cramerimplem2  22662  pmatcoe1fsupp  22679  mat2pmatbas  22704  mat2pmatmul  22709  mat2pmatlin  22713  decpmatmul  22750  monmatcollpw  22757  pm2mpf1  22777  pm2mpghm  22794  istps  22912  mretopd  23070  neiptopuni  23108  lpdifsn  23121  restcls  23159  perfopn  23163  pnfnei  23198  mnfnei  23199  lmss  23276  hauscmplem  23384  is2ndc  23424  2ndcdisj  23434  hausnlly  23471  txuni2  23543  ptpjpre1  23549  elpt  23550  dfac14  23596  xkococn  23638  fbasrn  23862  fin1aufil  23910  elfm2  23926  elfm3  23928  fbflim  23954  flffbas  23973  cnpflf2  23978  fclsbas  23999  efmndtmd  24079  tsmssubm  24121  iscusp2  24279  imasdsf1olem  24351  metustel  24528  metuel2  24543  isnghm  24701  opnreen  24810  iccpnfcnv  24924  ehleudisval  25399  ehl1eudis  25400  ehl2eudis  25402  minveclem3b  25408  ovoliunlem1  25482  ioombl1lem4  25541  subopnmbl  25584  vitalilem2  25589  vitalilem3  25590  mbfimaopnlem  25635  mbfimaopn2  25637  itg2l  25709  dvply1  26263  vieta1lem1  26290  vieta1lem2  26291  elaa  26296  taylthlem2  26354  taylthlem2OLD  26355  abelthlem6  26417  abelthlem9  26421  sinq34lt0t  26489  ellogrn  26539  dvrelog  26617  ellogdm  26619  logtayl2  26642  cxpcn3lem  26727  cxpcn3  26728  1cubr  26822  atandm  26856  atanf  26860  reasinsin  26876  atans2  26911  dmarea  26937  xrlimcnp  26948  amgmlem  26970  ppiublem1  27182  lgsdir2lem2  27306  gausslemma2dlem1a  27345  lgsquadlem1  27360  lgsquadlem2  27361  2sqlem1  27397  rpvmasum2  27492  madeval2  27842  newval  27844  leftval  27858  rightval  27859  lltr  27871  madess  27875  oldssmade  27876  oldss  27879  lrold  27906  addsproplem2  27979  addsproplem4  27981  addsproplem6  27983  negsproplem4  28040  negsproplem6  28042  precsexlem10  28225  precsexlem11  28226  ltonold  28270  elnns  28349  elzs  28393  edgiedgb  29140  isuhgr  29146  isushgr  29147  isupgr  29170  isumgr  29181  umgredg  29224  umgrpredgv  29226  umgredgne  29231  umgredgnlp  29233  isuspgr  29238  isusgr  29239  ausgrusgri  29254  usgredgppr  29282  edgssv2  29284  uspgredg2vlem  29309  uspgredg2v  29310  ushgredgedg  29315  ushgredgedgloop  29317  griedg0ssusgr  29351  uhgrissubgr  29361  subumgredg2  29371  uhgrspansubgrlem  29376  umgrres1lem  29396  upgrres1  29399  nbgrcl  29421  nbuhgr  29429  nbuhgr2vtx1edgblem  29437  nbupgrres  29450  edgnbusgreu  29453  nbusgredgeu0  29454  nbusgrf1o0  29455  hashnbusgrnn0  29462  nbupgruvtxres  29493  cffldtocusgr  29533  cffldtocusgrOLD  29534  cusgrfilem2  29543  vtxdg0v  29560  vtxduhgr0nedg  29579  uhgrvd00  29621  vtxdginducedm1  29630  finsumvtxdg2ssteplem4  29635  wlk1walk  29725  wlkp1lem6  29763  iswwlks  29922  wwlknllvtx  29932  wwlksonvtx  29941  wspthnonp  29945  wlkiswwlksupgr2  29963  wwlksnwwlksnon  30001  2pthon3v  30029  umgr2wlk  30035  elwwlks2s3  30037  wwlks2onv  30039  elwwlks2ons3im  30040  isclwwlk  30072  clwwlkccatlem  30077  clwlkclwwlk  30090  wwlksext2clwwlk  30145  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  clwwlknon1  30185  clwwlknon1nloop  30187  clwwlknon2x  30191  1pthon2v  30241  uhgr3cyclex  30270  isconngr  30277  isconngr1  30278  eucrctshift  30331  frgrnbnb  30381  frgrncvvdeqlem1  30387  frgrncvvdeqlem2  30388  frgrncvvdeqlem3  30389  frgrncvvdeqlem9  30395  fusgreghash2wspv  30423  extwwlkfab  30440  numclwwlk1lem2foa  30442  numclwwlk1lem2fo  30446  clwlknon2num  30456  numclwlk2lem2f1o  30467  numclwwlk5lem  30475  topnfbey  30557  isvclem  30666  isnvlem  30699  vsfval  30722  h2hlm  31069  hhcmpl  31289  hhcms  31292  elch0  31343  omlsilem  31491  h1de2ctlem  31644  elspansni  31647  nonbooli  31740  spansncvi  31741  adjeq  32024  cnlnssadj  32169  cnvbraval  32199  brabgaf  32697  2ndresdju  32740  fmptdF  32747  fmptcof2  32748  acunirnmpt  32750  acunirnmpt2  32751  ofpreima  32756  fcnvgreu  32763  fdifsuppconst  32780  1stpreima  32798  2ndpreima  32799  fz2ssnn0  32876  elxrge02  33009  ccatws1f1o  33029  gsumwrd2dccatlem  33156  psgnfzto1stlem  33179  cycpmgcl  33232  elrgspnlem1  33321  elrgspnlem2  33322  elrgspnlem4  33324  elrgspnsubrunlem1  33326  domnprodeq0  33355  nsgqusf1olem2  33492  nsgqusf1olem3  33493  prmidl0  33528  crngmxidl  33547  opprnsg  33562  rprmirredb  33610  zringfrac  33632  evl1deg2  33655  evl1deg3  33656  ply1degltel  33672  ply1degleel  33673  evlextv  33704  esplyfval3  33734  esplyindfv  33738  esplyfvn  33739  vietalem  33741  fldextrspunlsplem  33836  isconstr  33899  constrsuc  33901  constrconj  33908  submatres  33969  lmat22lem  33980  crefdf  34011  cmppcmp  34021  rspectopn  34030  prsdm  34077  prsrn  34078  xrge0iifcnv  34096  xrge0iifiso  34098  xrge0iifhom  34100  pnfneige0  34114  qqhre  34183  rrhre  34184  esumnul  34211  esumcvgsum  34251  ldgenpisyslem1  34326  measvuni  34377  cntnevol  34391  dya2iocnrect  34444  sibf0  34497  oddpwdc  34517  eulerpartlemd  34529  eulerpartgbij  34535  eulerpartlemgh  34541  isrrvv  34606  coinfliprv  34646  ballotlem7  34699  signswch  34724  hashreprin  34783  chtvalz  34792  circlemethhgt  34806  hgt750lemb  34819  tgoldbachgt  34826  bnj23  34880  bnj158  34891  bnj168  34892  bnj1138  34950  bnj1143  34951  bnj1454  35003  bnj110  35019  bnj882  35087  bnj893  35089  bnj916  35094  bnj970  35108  bnj983  35112  bnj984  35113  bnj1137  35156  bnj1174  35164  bnj1388  35194  bnj1398  35195  r1wf  35258  onvf1odlem4  35307  loop1cycl  35338  subfacp1lem5  35385  satfv1  35564  satfrnmapom  35571  satf0op  35578  satf0n0  35579  fmlafvel  35586  fmlaomn0  35591  fmlan0  35592  satffunlem2lem2  35607  satfv0fvfmla0  35614  satefvfmla0  35619  mrsub0  35717  mrsubccat  35719  mrsubcn  35720  elmrsubrn  35721  msubco  35732  msubvrs  35761  elmthm  35777  mthmblem  35781  ellcsrspsn  35842  elrn3  35963  dfon2lem7  35988  brsset  36088  eltrans  36090  elfix  36102  ellimits  36109  elfuns  36114  elsingles  36117  fvtransport  36233  brcolinear2  36259  fvray  36342  linedegen  36344  fvline  36345  ellines  36353  fwddifn0  36365  elhf  36375  hfninf  36387  rmoeqi  36388  rmoeqbii  36389  reueqi  36390  reueqbii  36391  rabeqbii  36395  iuneq12i  36396  iineq1i  36397  iineq12i  36398  riotaeqbii  36399  ixpeq1i  36401  itgeq12i  36407  cbvprodvw2  36448  fnessref  36558  ttctr  36694  bj-ififc  36866  bj-csbsnlem  37229  bj-elgab  37265  currysetlem1  37273  bj-eltag  37303  bj-sngltag  37309  bj-projun  37320  bj-velpwALT  37379  bj-0nelmpt  37447  bj-opelidres  37494  bj-inftyexpitaudisj  37538  bj-elccinfty  37547  f1omptsnlem  37669  icoreelrnab  37687  relowlpssretop  37697  rdgssun  37711  exrecfnlem  37712  finxpnom  37734  uncov  37939  tan2h  37950  ptrecube  37958  poimirlem25  37983  poimirlem29  37987  poimirlem30  37988  poimirlem31  37989  poimirlem32  37990  cnambfre  38006  ftc1cnnc  38030  sdclem2  38080  sdclem1  38081  fdc  38083  caushft  38099  issmgrpOLD  38201  ismndo  38210  isrngo  38235  isdivrngo  38288  csbcom2fi  38466  elecALTV  38609  brrabga  38679  eldmxrncnvepres  38772  eldmxrncnvepres2  38773  elrels2  38779  blockadjliftmap  38796  dfpre  38814  eupre  38832  eldmcoss  38886  coss0  38907  petseq  39314  dath  40199  diclspsn  41657  dvh4dimlem  41906  dvh2dim  41908  dvh3dim3N  41912  lcfrvalsnN  42004  mapdh6eN  42203  mapdh7dN  42213  mapdh8b  42243  hdmap1l6e  42277  lcmfunnnd  42468  3factsumint1  42477  primrootsunit1  42553  primrootscoprmpow  42555  aks6d1c2lem4  42583  sticksstones2  42603  sticksstones3  42604  sticksstones10  42611  sticksstones12a  42613  sticksstones12  42614  aks6d1c6lem2  42627  aks6d1c6lem3  42628  redvmptabs  42809  readvrec2  42810  readvrec  42811  frlmfielbas  42962  mhpind  43044  pellex  43284  rmspecnonsq  43356  islmodfg  43518  aaitgo  43611  areaquad  43665  ordeldif1o  43709  naddwordnexlem4  43850  fpwfvss  43860  finona1cl  43901  elcnvcnvintab  44030  elnonrel  44033  elcnvcnvlem  44047  cnvcnvintabd  44048  brfvrcld2  44140  grur1cld  44680  dvgrat  44760  cvgdvgrat  44761  radcnvrat  44762  nznngen  44764  uzmptshftfval  44794  binomcxplemcvg  44802  binomcxplemnotnn0  44804  tpid3gVD  45289  en3lplem2VD  45291  orbitclmpt  45406  wfaxrep  45442  wfaxsep  45443  wfaxpow  45445  wfaxpr  45446  wfaxun  45447  wfac8prim  45450  brpermmodelcnv  45452  nregmodellem  45464  iuneq1i  45536  rexanuz3  45547  eliuniin  45550  eliuniin2  45571  disjinfi  45643  fsneq  45656  iuneqfzuzlem  45785  allbutfi  45843  eluzelz2  45852  uz0  45861  uzublem  45879  uzid3  45884  elicores  45984  uzinico  46010  climsuselem1  46058  climsuse  46059  islptre  46070  fnlimfvre  46123  limsupresico  46149  limsupvaluz  46157  limsupubuzlem  46161  limsupequzmptlem  46177  liminfresico  46220  cnrefiisplem  46278  stoweidlem14  46463  stoweidlem39  46488  stoweidlem48  46497  stoweidlem51  46500  stoweidlem59  46508  stoweidlem62  46511  wallispilem3  46516  fourierdlem42  46598  fourierdlem62  46617  fourierdlem80  46635  fourierdlem103  46658  fourierdlem104  46659  etransclem26  46709  rrxsnicc  46749  ioorrnopn  46754  ioorrnopnxr  46756  sge00  46825  sge0fodjrnlem  46865  sge0isum  46876  sge0seq  46895  meadjiunlem  46914  carageneld  46951  volicorescl  47002  hoidmv1lelem1  47040  hoidmv1le  47043  hoidmvlelem1  47044  hoidmvlelem3  47046  ovnhoilem2  47051  hoiqssbllem2  47072  opnvonmbllem2  47082  ovolval4lem1  47098  iinhoiicc  47123  vonioolem1  47129  smflimlem1  47220  smflimlem2  47221  smflim  47226  nsssmfmbf  47228  smfresal  47237  smfrec  47238  smfdiv  47246  smfpimbor1lem2  47248  smflim2  47255  smflimmpt  47259  smfinflem  47266  smflimsuplem1  47269  smflimsuplem2  47270  smflimsuplem3  47271  smflimsuplem5  47273  smflimsuplem6  47274  smflimsup  47277  smflimsupmpt  47278  smfliminfmpt  47281  chnerlem1  47331  chnerlem2  47332  tannpoly  47353  sinnpoly  47354  fcores  47530  ndmaovcl  47666  ndmaovcom  47668  ndmaovass  47669  ndmaovdistr  47670  dfatco  47719  otiunsndisjX  47742  fvmptrabdm  47756  ceilhalfelfzo1  47797  modmknepk  47831  elsetpreimafvb  47859  sprsymrelfolem2  47968  sprsymrelf  47970  sprsymrelf1  47971  prpair  47976  prproropf1olem0  47977  paireqne  47986  fmtno4prmfac  48050  dfodd5  48151  sbgoldbo  48278  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  clnbgrcl  48312  clnbgredg  48331  sclnbgrel  48338  isubgredg  48357  uhgrimedgi  48381  isuspgrim0  48385  isuspgrimlem  48386  gricushgr  48408  clnbgrgrimlem  48424  grimedg  48426  usgrgrtrirex  48441  stgrnbgr0  48455  isubgr3stgrlem3  48459  isubgr3stgrlem4  48460  isubgr3stgrlem6  48462  isubgr3stgrlem7  48463  uspgrlimlem2  48480  uspgrlimlem3  48481  grlimedgclnbgr  48486  grlimprclnbgr  48487  grlimprclnbgrvtx  48490  grlimgrtrilem2  48493  usgrexmpl2trifr  48528  gpgvtxel  48538  gpgedgel  48541  gpgusgralem  48547  gpg5order  48551  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgnbgrvtx0  48565  gpgnbgrvtx1  48566  gpg5nbgrvtx03star  48571  gpg5nbgr3star  48572  gpgvtxdg3  48573  gpg5gricstgr3  48581  gpgprismgr4cycllem3  48588  gpgprismgr4cycllem7  48592  gpgprismgr4cycllem8  48593  gpgprismgr4cycllem10  48595  pgnbgreunbgrlem3  48609  pgnbgreunbgrlem6  48615  pgnbgreunbgr  48616  uspgrsprf  48637  uspgrsprf1  48638  uspgrsprfo  48639  ply1sclrmsm  48875  lcoop  48902  lincfsuppcl  48904  linccl  48905  lincvalsng  48907  lincvalpr  48909  lincvalsc0  48912  linc0scn0  48914  lincdifsn  48915  linc1  48916  lincsum  48920  lincscm  48921  lspsslco  48928  snlindsntor  48962  lincresunit3lem2  48971  ldepsnlinclem1  48996  ldepsnlinclem2  48997  prelrrx2  49204  prelrrx2b  49205  rrx2xpref1o  49209  rrx2plord  49211  rrx2linesl  49234  sectrcl  49512  invrcl  49514  initopropdlemlem  49729  initopropd  49733  termopropd  49734  zeroopropd  49735  oppcthin  49928  indthinc  49952  prsthinc  49954  elpglem3  50203