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 ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

This proof depends on syntax axioms:   ↔ wb 105   = wceq 1402   ∈ wcel 2209

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used 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  3754  tpid3g  3828  oprcl  3928  elunirab  3948  elintrab  3982  exss  4367  elop  4371  opm  4374  brabsb  4403  brabga  4406  pofun  4457  elsuci  4548  elsucg  4549  elsuc2g  4550  ordsucim  4647  peano2  4742  elxp  4791  brab2a  4828  brab2ga  4850  elco  4946  elcnv  4957  dmmrnm  5001  elrnmptg  5034  opelres  5068  rninxp  5231  eliota  5365  funco  5417  elfv  5693  nfvres  5732  fvopab3g  5778  fvmptssdm  5790  fmptco  5874  funfvima  5950  fliftel  5999  acexmidlema  6076  acexmidlemb  6077  acexmidlem2  6082  eloprabga  6175  elrnmpo  6202  ovid  6205  offval  6310  xporderlem  6467  brtpos2  6522  issmo  6559  smores3  6564  tfrlem7  6588  tfrlem9  6590  tfr0dm  6593  tfri2  6637  rdgon  6657  freccllem  6673  frecfcllem  6675  frecsuclem  6677  el1o  6710  dif1o  6711  nnsucuniel  6768  elecg  6847  brecop  6899  erovlem  6901  oviec  6915  mapsncnv  6977  mptelixpg  7016  isfi  7047  enssdom  7048  map1  7101  xpcomco  7124  exmidpw  7215  exmidpweq  7216  tpfidceq  7237  fnfi  7250  fidcenumlemrks  7270  fidcenumlemrk  7271  djulclb  7395  eldju  7408  eldju2ndl  7412  eldju2ndr  7413  ctssdccl  7451  pw1nel3  7590  sucpw1nel3  7592  elni  7675  nlt1pig  7708  0nnq  7731  dfmq0qs  7796  dfplq0qs  7797  nqnq0  7808  elinp  7841  0npr  7850  ltdfpr  7873  nqprl  7918  nqpru  7919  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemfl  7942  mulnqprlemfu  7943  cauappcvgprlemladdru  8023  suplocexprlemell  8080  addsrpr  8112  mulsrpr  8113  opelcn  8193  opelreal  8194  elreal  8195  elreal2  8197  0ncn  8198  addcnsr  8201  mulcnsr  8202  addvalex  8211  peano1nnnn  8219  peano2nnnn  8220  xrlenlt  8390  1nn  9315  peano2nn  9316  elnn0  9565  elnnne0  9577  un0addcl  9596  un0mulcl  9597  elxnn0  9632  uztrn2  9940  elnnuz  9959  elnn0uz  9960  elq  10022  elxr  10178  elfzm1b  10505  fz01or  10518  infssuzex  10666  infssfzcldc  10669  infssfzledc  10670  frecfzennn  10863  inftonninf  10879  seqf  10901  ser0  10970  ser0f  10971  hashinfom  11217  iswrd  11306  pfxccatpfx1  11508  clim2ser  12103  clim2ser2  12104  isermulc2  12106  iserle  12108  climserle  12111  fsum3cvg3  12163  isumclim3  12190  isumadd  12198  sumsplitdc  12199  iserabs  12242  cvgcmpub  12243  isumshft  12257  isumsplit  12258  isumlessdc  12263  cvgratz  12299  cvgratgt0  12300  clim2prod  12306  clim2divap  12307  prodf1  12309  zproddc  12346  prodsnf  12359  divides  12556  dvdsflip  12618  nninfctlemfo  12817  ialgrlemconst  12821  prm23lt5  13042  4sqlem2  13168  4sqlem12  13181  ballotfilemfrcn0  13273  ballotfilem7  13279  ennnfonelemjn  13293  ennnfonelem1  13298  ennnfonelemdm  13311  basmex  13412  ghmeqker  14074  opprringb  14386  isrhm  14465  rrgmex  14569  lssmex  14692  lidlmex  14812  2idlmex  14838  df2idl2  14846  2idlss  14851  psrbagf  15054  istps  15133  lmss  15347  txuni2  15357  dvply1  15866  sinq34lt0t  15932  logfac  15995  lgsdir2lem2  16148  gausslemma2dlem1a  16177  lgsquadlem1  16196  lgsquadlem2  16197  2sqlem1  16233  isuhgrm  16312  isushgrm  16313  isupgren  16336  isumgren  16346  umgredg  16386  umgrpredgv  16388  umgredgne  16391  umgredgnlp  16393  isuspgren  16398  isusgren  16399  ausgrusgrien  16412  usgredgppren  16438  edgssv2en  16440  uspgredg2vlem  16461  uspgredg2v  16462  ushgredgedg  16467  ushgredgedgloop  16469  griedg0ssusgr  16492  uhgrissubgr  16502  subumgredg2en  16512  uhgrspansubgrlem  16517  vtxedgfi  16530  vtxlpfi  16531  vtxdg0v  16535  wlk1walkdom  16600  clwwlkccatlem  16641  clwwlknnn  16653  clwwlknon2x  16676  bdceq  16868  bj-nntrans  16977  bj-nnelirr  16979  ss1oel2o  17017  wexmiddifxylem  17045  trilpolemisumle  17087