Theorem eleq2i 2237

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

Syntax hints:   ↔ wb 104   = wceq 1348   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eleq12i  2238  eleqtri  2245  eleq2s  2265  hbxfreq  2277  abeq2i  2281  abeq1i  2282  nfceqi  2308  raleqbii  2482  rexeqbii  2483  rabeq2i  2727  elab2g  2877  elrabf  2884  elrab3t  2885  elrab2  2889  cbvsbcw  2982  cbvsbc  2983  csbcow  3060  elin2  3315  dfnul2  3416  noel  3418  rabn0m  3442  rabeq0  3444  eltpg  3628  tpid3g  3698  oprcl  3789  elunirab  3809  elintrab  3843  exss  4212  elop  4216  opm  4219  brabsb  4246  brabga  4249  pofun  4297  elsuci  4388  elsucg  4389  elsuc2g  4390  ordsucim  4484  peano2  4579  elxp  4628  brab2a  4664  brab2ga  4686  elco  4777  elcnv  4788  dmmrnm  4830  elrnmptg  4863  opelres  4896  rninxp  5054  eliota  5186  funco  5238  elfv  5494  nfvres  5529  fvopab3g  5569  fvmptssdm  5580  fmptco  5662  funfvima  5727  fliftel  5772  acexmidlema  5844  acexmidlemb  5845  acexmidlem2  5850  eloprabga  5940  elrnmpo  5966  ovid  5969  offval  6068  xporderlem  6210  brtpos2  6230  issmo  6267  smores3  6272  tfrlem7  6296  tfrlem9  6298  tfr0dm  6301  tfri2  6345  rdgon  6365  freccllem  6381  frecfcllem  6383  frecsuclem  6385  el1o  6416  dif1o  6417  nnsucuniel  6474  elecg  6551  brecop  6603  erovlem  6605  oviec  6619  mapsncnv  6673  mptelixpg  6712  isfi  6739  enssdom  6740  map1  6790  xpcomco  6804  exmidpw  6886  exmidpweq  6887  fnfi  6914  fidcenumlemrks  6930  fidcenumlemrk  6931  djulclb  7032  eldju  7045  eldju2ndl  7049  eldju2ndr  7050  ctssdccl  7088  pw1nel3  7208  sucpw1nel3  7210  elni  7270  nlt1pig  7303  0nnq  7326  dfmq0qs  7391  dfplq0qs  7392  nqnq0  7403  elinp  7436  0npr  7445  ltdfpr  7468  nqprl  7513  nqpru  7514  addnqprlemfl  7521  addnqprlemfu  7522  mulnqprlemfl  7537  mulnqprlemfu  7538  cauappcvgprlemladdru  7618  suplocexprlemell  7675  addsrpr  7707  mulsrpr  7708  opelcn  7788  opelreal  7789  elreal  7790  elreal2  7792  0ncn  7793  addcnsr  7796  mulcnsr  7797  addvalex  7806  peano1nnnn  7814  peano2nnnn  7815  xrlenlt  7984  1nn  8889  peano2nn  8890  elnn0  9137  elnnne0  9149  un0addcl  9168  un0mulcl  9169  elxnn0  9200  uztrn2  9504  elnnuz  9523  elnn0uz  9524  elq  9581  elxr  9733  elfzm1b  10054  fz01or  10067  frecfzennn  10382  inftonninf  10397  seqf  10417  ser0  10470  ser0f  10471  hashinfom  10712  clim2ser  11300  clim2ser2  11301  isermulc2  11303  iserle  11305  climserle  11308  fsum3cvg3  11359  isumclim3  11386  isumadd  11394  sumsplitdc  11395  iserabs  11438  cvgcmpub  11439  isumshft  11453  isumsplit  11454  isumlessdc  11459  cvgratz  11495  cvgratgt0  11496  clim2prod  11502  clim2divap  11503  prodf1  11505  zproddc  11542  prodsnf  11555  divides  11751  dvdsflip  11811  infssuzex  11904  ialgrlemconst  11997  prm23lt5  12217  4sqlem2  12341  ennnfonelemjn  12357  ennnfonelem1  12362  ennnfonelemdm  12375  basmex  12474  istps  12824  lmss  13040  txuni2  13050  sinq34lt0t  13546  lgsdir2lem2  13724  2sqlem1  13744  bdceq  13877  bj-nntrans  13986  bj-nnelirr  13988  ss1oel2o  14026  trilpolemisumle  14070