Theorem eleq2i 2273

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

Syntax hints:   ↔ wb 105   = wceq 1373   ∈ wcel 2177

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  eleq12i  2274  eleqtri  2281  eleq2s  2301  hbxfreq  2313  abeq2i  2317  abeq1i  2318  nfceqi  2345  raleqbii  2519  rexeqbii  2520  rabeq2i  2770  elab2g  2924  elrabf  2931  elrab3t  2932  elrab2  2936  cbvsbcw  3030  cbvsbc  3031  csbcow  3108  elin2  3365  dfnul2  3466  noel  3468  rabn0m  3492  rabeq0  3494  eltpg  3683  tpid3g  3753  oprcl  3849  elunirab  3869  elintrab  3903  exss  4279  elop  4283  opm  4286  brabsb  4315  brabga  4318  pofun  4367  elsuci  4458  elsucg  4459  elsuc2g  4460  ordsucim  4556  peano2  4651  elxp  4700  brab2a  4736  brab2ga  4758  elco  4852  elcnv  4863  dmmrnm  4906  elrnmptg  4939  opelres  4973  rninxp  5135  eliota  5268  funco  5320  elfv  5587  nfvres  5623  fvopab3g  5665  fvmptssdm  5677  fmptco  5759  funfvima  5829  fliftel  5875  acexmidlema  5948  acexmidlemb  5949  acexmidlem2  5954  eloprabga  6045  elrnmpo  6072  ovid  6075  offval  6179  xporderlem  6330  brtpos2  6350  issmo  6387  smores3  6392  tfrlem7  6416  tfrlem9  6418  tfr0dm  6421  tfri2  6465  rdgon  6485  freccllem  6501  frecfcllem  6503  frecsuclem  6505  el1o  6536  dif1o  6537  nnsucuniel  6594  elecg  6673  brecop  6725  erovlem  6727  oviec  6741  mapsncnv  6795  mptelixpg  6834  isfi  6865  enssdom  6866  map1  6918  xpcomco  6936  exmidpw  7020  exmidpweq  7021  tpfidceq  7042  fnfi  7053  fidcenumlemrks  7070  fidcenumlemrk  7071  djulclb  7172  eldju  7185  eldju2ndl  7189  eldju2ndr  7190  ctssdccl  7228  pw1nel3  7362  sucpw1nel3  7364  elni  7441  nlt1pig  7474  0nnq  7497  dfmq0qs  7562  dfplq0qs  7563  nqnq0  7574  elinp  7607  0npr  7616  ltdfpr  7639  nqprl  7684  nqpru  7685  addnqprlemfl  7692  addnqprlemfu  7693  mulnqprlemfl  7708  mulnqprlemfu  7709  cauappcvgprlemladdru  7789  suplocexprlemell  7846  addsrpr  7878  mulsrpr  7879  opelcn  7959  opelreal  7960  elreal  7961  elreal2  7963  0ncn  7964  addcnsr  7967  mulcnsr  7968  addvalex  7977  peano1nnnn  7985  peano2nnnn  7986  xrlenlt  8157  1nn  9067  peano2nn  9068  elnn0  9317  elnnne0  9329  un0addcl  9348  un0mulcl  9349  elxnn0  9380  uztrn2  9686  elnnuz  9705  elnn0uz  9706  elq  9763  elxr  9918  elfzm1b  10240  fz01or  10253  infssuzex  10398  frecfzennn  10593  inftonninf  10609  seqf  10631  ser0  10700  ser0f  10701  hashinfom  10945  iswrd  11018  clim2ser  11723  clim2ser2  11724  isermulc2  11726  iserle  11728  climserle  11731  fsum3cvg3  11782  isumclim3  11809  isumadd  11817  sumsplitdc  11818  iserabs  11861  cvgcmpub  11862  isumshft  11876  isumsplit  11877  isumlessdc  11882  cvgratz  11918  cvgratgt0  11919  clim2prod  11925  clim2divap  11926  prodf1  11928  zproddc  11965  prodsnf  11978  divides  12175  dvdsflip  12237  nninfctlemfo  12436  ialgrlemconst  12440  prm23lt5  12661  4sqlem2  12787  4sqlem12  12800  ennnfonelemjn  12848  ennnfonelem1  12853  ennnfonelemdm  12866  basmex  12966  ghmeqker  13682  isrhm  13995  rrgmex  14098  lssmex  14192  lidlmex  14312  2idlmex  14338  df2idl2  14346  2idlss  14351  psrbagf  14507  istps  14579  lmss  14793  txuni2  14803  dvply1  15312  sinq34lt0t  15378  lgsdir2lem2  15581  gausslemma2dlem1a  15610  lgsquadlem1  15629  lgsquadlem2  15630  2sqlem1  15666  isuhgrm  15742  isushgrm  15743  isupgren  15766  isumgren  15776  bdceq  15916  bj-nntrans  16025  bj-nnelirr  16027  ss1oel2o  16066  trilpolemisumle  16118