Theorem eleq2i 2305

Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eleq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eleq2i	⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Proof of Theorem eleq2i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eleq2 2302	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Syntax hints:   ↔ wb 105   = wceq 1402   ∈ wcel 2209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  eleq12i  2306  eleqtri  2313  eleq2s  2333  hbxfreq  2345  abeq2i  2349  abeq1i  2350  nfceqi  2388  raleqbii  2562  rexeqbii  2563  reqabi  2728  rabeq2i  2818  elab2g  2973  elrabf  2980  elrab3t  2981  elrab2  2985  cbvsbcw  3079  cbvsbc  3080  csbcow  3158  elin2  3417  noel  3525  rabn0m  3549  rabeq0  3552  eltpg  3750  tpid3g  3823  oprcl  3923  elunirab  3943  elintrab  3977  exss  4362  elop  4366  opm  4369  brabsb  4398  brabga  4401  pofun  4452  elsuci  4543  elsucg  4544  elsuc2g  4545  ordsucim  4642  peano2  4737  elxp  4786  brab2a  4823  brab2ga  4845  elco  4941  elcnv  4952  dmmrnm  4996  elrnmptg  5029  opelres  5063  rninxp  5226  eliota  5360  funco  5412  elfv  5688  nfvres  5726  fvopab3g  5772  fvmptssdm  5784  fmptco  5865  funfvima  5940  fliftel  5989  acexmidlema  6066  acexmidlemb  6067  acexmidlem2  6072  eloprabga  6165  elrnmpo  6192  ovid  6195  offval  6300  xporderlem  6457  brtpos2  6512  issmo  6549  smores3  6554  tfrlem7  6578  tfrlem9  6580  tfr0dm  6583  tfri2  6627  rdgon  6647  freccllem  6663  frecfcllem  6665  frecsuclem  6667  el1o  6700  dif1o  6701  nnsucuniel  6758  elecg  6837  brecop  6889  erovlem  6891  oviec  6905  mapsncnv  6967  mptelixpg  7006  isfi  7037  enssdom  7038  map1  7091  xpcomco  7114  exmidpw  7205  exmidpweq  7206  tpfidceq  7227  fnfi  7240  fidcenumlemrks  7260  fidcenumlemrk  7261  djulclb  7385  eldju  7398  eldju2ndl  7402  eldju2ndr  7403  ctssdccl  7441  pw1nel3  7580  sucpw1nel3  7582  elni  7665  nlt1pig  7698  0nnq  7721  dfmq0qs  7786  dfplq0qs  7787  nqnq0  7798  elinp  7831  0npr  7840  ltdfpr  7863  nqprl  7908  nqpru  7909  addnqprlemfl  7916  addnqprlemfu  7917  mulnqprlemfl  7932  mulnqprlemfu  7933  cauappcvgprlemladdru  8013  suplocexprlemell  8070  addsrpr  8102  mulsrpr  8103  opelcn  8183  opelreal  8184  elreal  8185  elreal2  8187  0ncn  8188  addcnsr  8191  mulcnsr  8192  addvalex  8201  peano1nnnn  8209  peano2nnnn  8210  xrlenlt  8380  1nn  9294  peano2nn  9295  elnn0  9544  elnnne0  9556  un0addcl  9575  un0mulcl  9576  elxnn0  9611  uztrn2  9919  elnnuz  9938  elnn0uz  9939  elq  10001  elxr  10157  elfzm1b  10483  fz01or  10496  infssuzex  10644  infssfzcldc  10647  infssfzledc  10648  frecfzennn  10841  inftonninf  10857  seqf  10879  ser0  10948  ser0f  10949  hashinfom  11195  iswrd  11284  pfxccatpfx1  11486  clim2ser  12081  clim2ser2  12082  isermulc2  12084  iserle  12086  climserle  12089  fsum3cvg3  12141  isumclim3  12168  isumadd  12176  sumsplitdc  12177  iserabs  12220  cvgcmpub  12221  isumshft  12235  isumsplit  12236  isumlessdc  12241  cvgratz  12277  cvgratgt0  12278  clim2prod  12284  clim2divap  12285  prodf1  12287  zproddc  12324  prodsnf  12337  divides  12534  dvdsflip  12596  nninfctlemfo  12795  ialgrlemconst  12799  prm23lt5  13020  4sqlem2  13146  4sqlem12  13159  ballotfilemfrcn0  13251  ballotfilem7  13257  ennnfonelemjn  13271  ennnfonelem1  13276  ennnfonelemdm  13289  basmex  13390  ghmeqker  14051  opprringb  14359  isrhm  14438  rrgmex  14542  lssmex  14664  lidlmex  14784  2idlmex  14810  df2idl2  14818  2idlss  14823  psrbagf  14977  istps  15056  lmss  15270  txuni2  15280  dvply1  15789  sinq34lt0t  15855  logfac  15918  lgsdir2lem2  16062  gausslemma2dlem1a  16091  lgsquadlem1  16110  lgsquadlem2  16111  2sqlem1  16147  isuhgrm  16226  isushgrm  16227  isupgren  16250  isumgren  16260  umgredg  16300  umgrpredgv  16302  umgredgne  16305  umgredgnlp  16307  isuspgren  16312  isusgren  16313  ausgrusgrien  16326  usgredgppren  16352  edgssv2en  16354  uspgredg2vlem  16375  uspgredg2v  16376  ushgredgedg  16381  ushgredgedgloop  16383  griedg0ssusgr  16406  uhgrissubgr  16416  subumgredg2en  16426  uhgrspansubgrlem  16431  vtxedgfi  16444  vtxlpfi  16445  vtxdg0v  16449  wlk1walkdom  16514  clwwlkccatlem  16555  clwwlknnn  16567  clwwlknon2x  16590  bdceq  16782  bj-nntrans  16891  bj-nnelirr  16893  ss1oel2o  16931  trilpolemisumle  16992