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 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 2708

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

This theorem is referenced by:  eleq12i  2829  eleqtri  2834  eleq2s  2854  hbxfreq  2866  nfceqi  2895  raleqbii  3309  rexeqbii  3310  rabeqi  3402  rabrabi  3408  reqabi  3412  elab2gw  3621  elab2g  3623  elrabf  3631  elrab3t  3633  elrab2  3637  cbvsbcw  3761  cbvsbcvw  3762  cbvsbc  3763  elin2  4143  elsymdif  4198  noel  4278  eltpg  4630  elunirab  4865  elintrab  4902  disjxiun  5082  exss  5415  otiunsndisj  5474  brabsb  5486  brabga  5489  epelg  5532  pofun  5557  elxp  5654  opeliunxp  5698  opeliun2xp  5699  bropaex12  5722  brab2a  5724  elcnv  5831  dmopabelb  5871  elrnmptg  5916  elres  5985  elimampt  6008  elrid  6011  cnv0  6103  rninxp  6143  elid  6163  elsuci  6392  elsucg  6393  elsuc2g  6394  elfv  6838  0fv  6881  opabiota  6922  dffv2  6935  fvopab3g  6942  fvmptex  6962  fvopab5  6981  fvn0ssdmfun  7026  fveqressseq  7031  f0cli  7050  fmptco  7082  fvrnressn  7115  funfvima  7185  elunirnALT  7207  fliftel  7264  eloprabga  7476  elrnmpo  7503  elimampo  7504  ovid  7508  offval  7640  1st2val  7970  2nd2val  7971  bropopvvv  8040  bropfvvvv  8042  fsplit  8067  xporderlem  8077  frpoins3xpg  8090  frpoins3xp3g  8091  brtpos2  8182  frrlem8  8243  frrlem9  8244  frrlem10  8245  fprresex  8260  issmo  8288  smores3  8293  tfrlem7  8322  tfrlem9  8324  tfrlem9a  8325  tfr2b  8335  tfr2  8337  rdgsuc  8363  frsucmptn  8378  tz7.48-2  8381  el1o  8430  ord2eln012  8432  dif1o  8435  ondif2  8437  oawordeulem  8489  elecg  8688  brecop  8757  erovlem  8760  eceqoveq  8769  mapsncnv  8841  mptelixpg  8883  brsdom  8921  isfi  8922  enssdomOLD  8924  brdom2  8929  xpcomco  9005  brsdom2  9039  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  11210  elnn0  12439  elnnne0  12451  un0addcl  12470  un0mulcl  12471  elxnn0  12512  uztrn2  12807  elnnuz  12828  elnn0uz  12829  elq  12900  elxr  13067  elfzm1b  13556  elfz0lmr  13738  uzrdgfni  13920  fzennn  13930  ser0  14016  hash2pwpr  14438  iswrd  14477  pfxccatpfx1  14698  s3iunsndisj  14930  sumz  15684  sumss  15686  fsumcvg3  15691  abscvgcvg  15782  isumshft  15804  prodf1  15856  prodeq1i  15881  zprod  15902  prod1  15909  prodss  15912  prodsn  15927  prodsnf  15929  bpolydiflem  16019  bpoly2  16022  bpoly3  16023  bpoly4  16024  ruclem6  16202  divides  16223  dvdsflip  16286  pwp1fsum  16360  sadc0  16423  eulerthlem2  16752  prm23lt5  16785  4sqlem2  16920  4sqlem12  16927  vdwpc  16951  xpscf  17529  cidpropd  17676  oppcsect  17745  funcpropd  17869  natpropd  17946  dfinito2  17970  dftermo2  17971  initoeu2lem0  17980  arwhoma  18012  eldmcoa  18032  pospo  18309  psss  18546  ex-chn1  18603  ex-chn2  18604  ismgmn0  18610  gsumpropd2lem  18647  elefmndbas  18841  smndex1basss  18876  smndex1mgm  18878  pwmnd  18908  dfgrp2e  18939  mulgfval  19045  eqg0subg  19171  cycsubmel  19175  ghmeqker  19218  elcntr  19305  cntri  19307  cntzsgrpcl  19309  oppgsubg  19338  fvcosymgeq  19404  symgfixels  19409  pmtrfrn  19433  efgsfo  19714  efgrelexlemb  19725  lt6abl  19870  dmdprd  19975  dprdval  19980  dprdw  19987  srgbinomlem4  20210  isnirred  20400  isrhm  20458  issrng  20821  lspexchn2  21129  lspindp2l  21132  lspindp2  21133  lbsextlem2  21157  rnglidl1  21230  df2idl2  21255  2idlss  21260  rngqiprngimfo  21299  cnfldfun  21366  pzriprnglem3  21463  pzriprnglem4  21464  pzriprnglem7  21467  pzriprnglem8  21468  pzriprnglem9  21469  pzriprnglem12  21472  pzriprnglem14  21474  dsmmelbas  21719  frlmbas3  21756  lindsind2  21799  islindf4  21818  psrbagf  21898  evlslem4  22054  psdmul  22132  ply1bascl2  22168  cply1mul  22261  lply1binom  22275  matsubgcell  22399  matinvgcell  22400  matvscacell  22401  matepmcl  22427  matepm2cl  22428  scmatscm  22478  smatvscl  22489  marrepcl  22529  marepvcl  22534  mulmarep1el  22537  mulmarep1gsum1  22538  mulmarep1gsum2  22539  submabas  22543  m1detdiag  22562  mdetdiag  22564  m2detleib  22596  gsummatr01lem3  22622  gsummatr01  22624  smadiadetlem4  22634  slesolinv  22645  slesolinvbi  22646  slesolex  22647  cramerimplem2  22649  pmatcoe1fsupp  22666  mat2pmatbas  22691  mat2pmatmul  22696  mat2pmatlin  22700  decpmatmul  22737  monmatcollpw  22744  pm2mpf1  22764  pm2mpghm  22781  istps  22899  mretopd  23057  neiptopuni  23095  lpdifsn  23108  restcls  23146  perfopn  23150  pnfnei  23185  mnfnei  23186  lmss  23263  hauscmplem  23371  is2ndc  23411  2ndcdisj  23421  hausnlly  23458  txuni2  23530  ptpjpre1  23536  elpt  23537  dfac14  23583  xkococn  23625  fbasrn  23849  fin1aufil  23897  elfm2  23913  elfm3  23915  fbflim  23941  flffbas  23960  cnpflf2  23965  fclsbas  23986  efmndtmd  24066  tsmssubm  24108  iscusp2  24266  imasdsf1olem  24338  metustel  24515  metuel2  24530  isnghm  24688  opnreen  24797  iccpnfcnv  24911  ehleudisval  25386  ehl1eudis  25387  ehl2eudis  25389  minveclem3b  25395  ovoliunlem1  25469  ioombl1lem4  25528  subopnmbl  25571  vitalilem2  25576  vitalilem3  25577  mbfimaopnlem  25622  mbfimaopn2  25624  itg2l  25696  dvply1  26250  vieta1lem1  26276  vieta1lem2  26277  elaa  26282  taylthlem2  26339  abelthlem6  26401  abelthlem9  26405  sinq34lt0t  26473  ellogrn  26523  dvrelog  26601  ellogdm  26603  logtayl2  26626  cxpcn3lem  26711  cxpcn3  26712  1cubr  26806  atandm  26840  atanf  26844  reasinsin  26860  atans2  26895  dmarea  26921  xrlimcnp  26932  amgmlem  26953  ppiublem1  27165  lgsdir2lem2  27289  gausslemma2dlem1a  27328  lgsquadlem1  27343  lgsquadlem2  27344  2sqlem1  27380  rpvmasum2  27475  madeval2  27825  newval  27827  leftval  27841  rightval  27842  lltr  27854  madess  27858  oldssmade  27859  oldss  27862  lrold  27889  addsproplem2  27962  addsproplem4  27964  addsproplem6  27966  negsproplem4  28023  negsproplem6  28025  precsexlem10  28208  precsexlem11  28209  ltonold  28253  elnns  28332  elzs  28376  edgiedgb  29123  isuhgr  29129  isushgr  29130  isupgr  29153  isumgr  29164  umgredg  29207  umgrpredgv  29209  umgredgne  29214  umgredgnlp  29216  isuspgr  29221  isusgr  29222  ausgrusgri  29237  usgredgppr  29265  edgssv2  29267  uspgredg2vlem  29292  uspgredg2v  29293  ushgredgedg  29298  ushgredgedgloop  29300  griedg0ssusgr  29334  uhgrissubgr  29344  subumgredg2  29354  uhgrspansubgrlem  29359  umgrres1lem  29379  upgrres1  29382  nbgrcl  29404  nbuhgr  29412  nbuhgr2vtx1edgblem  29420  nbupgrres  29433  edgnbusgreu  29436  nbusgredgeu0  29437  nbusgrf1o0  29438  hashnbusgrnn0  29445  nbupgruvtxres  29476  cffldtocusgr  29516  cusgrfilem2  29525  vtxdg0v  29542  vtxduhgr0nedg  29561  uhgrvd00  29603  vtxdginducedm1  29612  finsumvtxdg2ssteplem4  29617  wlk1walk  29707  wlkp1lem6  29745  iswwlks  29904  wwlknllvtx  29914  wwlksonvtx  29923  wspthnonp  29927  wlkiswwlksupgr2  29945  wwlksnwwlksnon  29983  2pthon3v  30011  umgr2wlk  30017  elwwlks2s3  30019  wwlks2onv  30021  elwwlks2ons3im  30022  isclwwlk  30054  clwwlkccatlem  30059  clwlkclwwlk  30072  wwlksext2clwwlk  30127  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  clwwlknon1  30167  clwwlknon1nloop  30169  clwwlknon2x  30173  1pthon2v  30223  uhgr3cyclex  30252  isconngr  30259  isconngr1  30260  eucrctshift  30313  frgrnbnb  30363  frgrncvvdeqlem1  30369  frgrncvvdeqlem2  30370  frgrncvvdeqlem3  30371  frgrncvvdeqlem9  30377  fusgreghash2wspv  30405  extwwlkfab  30422  numclwwlk1lem2foa  30424  numclwwlk1lem2fo  30428  clwlknon2num  30438  numclwlk2lem2f1o  30449  numclwwlk5lem  30457  topnfbey  30539  isvclem  30648  isnvlem  30681  vsfval  30704  h2hlm  31051  hhcmpl  31271  hhcms  31274  elch0  31325  omlsilem  31473  h1de2ctlem  31626  elspansni  31629  nonbooli  31722  spansncvi  31723  adjeq  32006  cnlnssadj  32151  cnvbraval  32181  brabgaf  32679  2ndresdju  32722  fmptdF  32729  fmptcof2  32730  acunirnmpt  32732  acunirnmpt2  32733  ofpreima  32738  fcnvgreu  32745  fdifsuppconst  32762  1stpreima  32780  2ndpreima  32781  fz2ssnn0  32858  elxrge02  32991  ccatws1f1o  33011  gsumwrd2dccatlem  33138  psgnfzto1stlem  33161  cycpmgcl  33214  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem4  33306  elrgspnsubrunlem1  33308  domnprodeq0  33337  nsgqusf1olem2  33474  nsgqusf1olem3  33475  prmidl0  33510  crngmxidl  33529  opprnsg  33544  rprmirredb  33592  zringfrac  33614  evl1deg2  33637  evl1deg3  33638  ply1degltel  33654  ply1degleel  33655  evlextv  33686  esplyfval3  33716  esplyindfv  33720  esplyfvn  33721  vietalem  33723  fldextrspunlsplem  33817  isconstr  33880  constrsuc  33882  constrconj  33889  submatres  33950  lmat22lem  33961  crefdf  33992  cmppcmp  34002  rspectopn  34011  prsdm  34058  prsrn  34059  xrge0iifcnv  34077  xrge0iifiso  34079  xrge0iifhom  34081  pnfneige0  34095  qqhre  34164  rrhre  34165  esumnul  34192  esumcvgsum  34232  ldgenpisyslem1  34307  measvuni  34358  cntnevol  34372  dya2iocnrect  34425  sibf0  34478  oddpwdc  34498  eulerpartlemd  34510  eulerpartgbij  34516  eulerpartlemgh  34522  isrrvv  34587  coinfliprv  34627  ballotlem7  34680  signswch  34705  hashreprin  34764  chtvalz  34773  circlemethhgt  34787  hgt750lemb  34800  tgoldbachgt  34807  bnj23  34861  bnj158  34872  bnj168  34873  bnj1138  34931  bnj1143  34932  bnj1454  34984  bnj110  35000  bnj882  35068  bnj893  35070  bnj916  35075  bnj970  35089  bnj983  35093  bnj984  35094  bnj1137  35137  bnj1174  35145  bnj1388  35175  bnj1398  35176  r1wf  35239  onvf1odlem4  35288  loop1cycl  35319  subfacp1lem5  35366  satfv1  35545  satfrnmapom  35552  satf0op  35559  satf0n0  35560  fmlafvel  35567  fmlaomn0  35572  fmlan0  35573  satffunlem2lem2  35588  satfv0fvfmla0  35595  satefvfmla0  35600  mrsub0  35698  mrsubccat  35700  mrsubcn  35701  elmrsubrn  35702  msubco  35713  msubvrs  35742  elmthm  35758  mthmblem  35762  ellcsrspsn  35823  elrn3  35944  dfon2lem7  35969  brsset  36069  eltrans  36071  elfix  36083  ellimits  36090  elfuns  36095  elsingles  36098  fvtransport  36214  brcolinear2  36240  fvray  36323  linedegen  36325  fvline  36326  ellines  36334  fwddifn0  36346  elhf  36356  hfninf  36368  rmoeqi  36369  rmoeqbii  36370  reueqi  36371  reueqbii  36372  rabeqbii  36376  iuneq12i  36377  iineq1i  36378  iineq12i  36379  riotaeqbii  36380  ixpeq1i  36382  itgeq12i  36388  cbvprodvw2  36429  fnessref  36539  ttctr  36675  bj-ififc  36847  bj-csbsnlem  37210  bj-elgab  37246  currysetlem1  37254  bj-eltag  37284  bj-sngltag  37290  bj-projun  37301  bj-velpwALT  37360  bj-0nelmpt  37428  bj-opelidres  37475  bj-inftyexpitaudisj  37519  bj-elccinfty  37528  f1omptsnlem  37652  icoreelrnab  37670  relowlpssretop  37680  rdgssun  37694  exrecfnlem  37695  finxpnom  37717  uncov  37922  tan2h  37933  ptrecube  37941  poimirlem25  37966  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  cnambfre  37989  ftc1cnnc  38013  sdclem2  38063  sdclem1  38064  fdc  38066  caushft  38082  issmgrpOLD  38184  ismndo  38193  isrngo  38218  isdivrngo  38271  csbcom2fi  38449  elecALTV  38592  brrabga  38662  eldmxrncnvepres  38755  eldmxrncnvepres2  38756  elrels2  38762  blockadjliftmap  38779  dfpre  38797  eupre  38815  eldmcoss  38869  coss0  38890  petseq  39297  dath  40182  diclspsn  41640  dvh4dimlem  41889  dvh2dim  41891  dvh3dim3N  41895  lcfrvalsnN  41987  mapdh6eN  42186  mapdh7dN  42196  mapdh8b  42226  hdmap1l6e  42260  lcmfunnnd  42451  3factsumint1  42460  primrootsunit1  42536  primrootscoprmpow  42538  aks6d1c2lem4  42566  sticksstones2  42586  sticksstones3  42587  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  aks6d1c6lem2  42610  aks6d1c6lem3  42611  redvmptabs  42792  readvrec2  42793  readvrec  42794  frlmfielbas  42945  mhpind  43027  pellex  43263  rmspecnonsq  43335  islmodfg  43497  aaitgo  43590  areaquad  43644  ordeldif1o  43688  naddwordnexlem4  43829  fpwfvss  43839  finona1cl  43880  elcnvcnvintab  44009  elnonrel  44012  elcnvcnvlem  44026  cnvcnvintabd  44027  brfvrcld2  44119  grur1cld  44659  dvgrat  44739  cvgdvgrat  44740  radcnvrat  44741  nznngen  44743  uzmptshftfval  44773  binomcxplemcvg  44781  binomcxplemnotnn0  44783  tpid3gVD  45268  en3lplem2VD  45270  orbitclmpt  45385  wfaxrep  45421  wfaxsep  45422  wfaxpow  45424  wfaxpr  45425  wfaxun  45426  wfac8prim  45429  brpermmodelcnv  45431  nregmodellem  45443  iuneq1i  45515  rexanuz3  45526  eliuniin  45529  eliuniin2  45550  disjinfi  45622  fsneq  45635  iuneqfzuzlem  45764  allbutfi  45822  eluzelz2  45831  uz0  45840  uzublem  45858  uzid3  45863  elicores  45963  uzinico  45989  climsuselem1  46037  climsuse  46038  islptre  46049  fnlimfvre  46102  limsupresico  46128  limsupvaluz  46136  limsupubuzlem  46140  limsupequzmptlem  46156  liminfresico  46199  cnrefiisplem  46257  stoweidlem14  46442  stoweidlem39  46467  stoweidlem48  46476  stoweidlem51  46479  stoweidlem59  46487  stoweidlem62  46490  wallispilem3  46495  fourierdlem42  46577  fourierdlem62  46596  fourierdlem80  46614  fourierdlem103  46637  fourierdlem104  46638  etransclem26  46688  rrxsnicc  46728  ioorrnopn  46733  ioorrnopnxr  46735  sge00  46804  sge0fodjrnlem  46844  sge0isum  46855  sge0seq  46874  meadjiunlem  46893  carageneld  46930  volicorescl  46981  hoidmv1lelem1  47019  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem3  47025  ovnhoilem2  47030  hoiqssbllem2  47051  opnvonmbllem2  47061  ovolval4lem1  47077  iinhoiicc  47102  vonioolem1  47108  smflimlem1  47199  smflimlem2  47200  smflim  47205  nsssmfmbf  47207  smfresal  47216  smfrec  47217  smfdiv  47225  smfpimbor1lem2  47227  smflim2  47234  smflimmpt  47238  smfinflem  47245  smflimsuplem1  47248  smflimsuplem2  47249  smflimsuplem3  47250  smflimsuplem5  47252  smflimsuplem6  47253  smflimsup  47256  smflimsupmpt  47257  smfliminfmpt  47260  chnerlem1  47312  chnerlem2  47313  tannpoly  47338  sinnpoly  47339  fcores  47515  ndmaovcl  47651  ndmaovcom  47653  ndmaovass  47654  ndmaovdistr  47655  dfatco  47704  otiunsndisjX  47727  fvmptrabdm  47741  ceilhalfelfzo1  47782  modmknepk  47816  elsetpreimafvb  47844  sprsymrelfolem2  47953  sprsymrelf  47955  sprsymrelf1  47956  prpair  47961  prproropf1olem0  47962  paireqne  47971  fmtno4prmfac  48035  dfodd5  48136  sbgoldbo  48263  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  clnbgrcl  48297  clnbgredg  48316  sclnbgrel  48323  isubgredg  48342  uhgrimedgi  48366  isuspgrim0  48370  isuspgrimlem  48371  gricushgr  48393  clnbgrgrimlem  48409  grimedg  48411  usgrgrtrirex  48426  stgrnbgr0  48440  isubgr3stgrlem3  48444  isubgr3stgrlem4  48445  isubgr3stgrlem6  48447  isubgr3stgrlem7  48448  uspgrlimlem2  48465  uspgrlimlem3  48466  grlimedgclnbgr  48471  grlimprclnbgr  48472  grlimprclnbgrvtx  48475  grlimgrtrilem2  48478  usgrexmpl2trifr  48513  gpgvtxel  48523  gpgedgel  48526  gpgusgralem  48532  gpg5order  48536  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgnbgrvtx0  48550  gpgnbgrvtx1  48551  gpg5nbgrvtx03star  48556  gpg5nbgr3star  48557  gpgvtxdg3  48558  gpg5gricstgr3  48566  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem7  48577  gpgprismgr4cycllem8  48578  gpgprismgr4cycllem10  48580  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  pgnbgreunbgr  48601  uspgrsprf  48622  uspgrsprf1  48623  uspgrsprfo  48624  ply1sclrmsm  48860  lcoop  48887  lincfsuppcl  48889  linccl  48890  lincvalsng  48892  lincvalpr  48894  lincvalsc0  48897  linc0scn0  48899  lincdifsn  48900  linc1  48901  lincsum  48905  lincscm  48906  lspsslco  48913  snlindsntor  48947  lincresunit3lem2  48956  ldepsnlinclem1  48981  ldepsnlinclem2  48982  prelrrx2  49189  prelrrx2b  49190  rrx2xpref1o  49194  rrx2plord  49196  rrx2linesl  49219  sectrcl  49497  invrcl  49499  initopropdlemlem  49714  initopropd  49718  termopropd  49719  zeroopropd  49720  oppcthin  49913  indthinc  49937  prsthinc  49939  elpglem3  50188