Theorem eleq2i 2244

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

Syntax hints:   ↔ wb 105   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleq12i  2245  eleqtri  2252  eleq2s  2272  hbxfreq  2284  abeq2i  2288  abeq1i  2289  nfceqi  2315  raleqbii  2489  rexeqbii  2490  rabeq2i  2735  elab2g  2885  elrabf  2892  elrab3t  2893  elrab2  2897  cbvsbcw  2991  cbvsbc  2992  csbcow  3069  elin2  3324  dfnul2  3425  noel  3427  rabn0m  3451  rabeq0  3453  eltpg  3638  tpid3g  3708  oprcl  3803  elunirab  3823  elintrab  3857  exss  4228  elop  4232  opm  4235  brabsb  4262  brabga  4265  pofun  4313  elsuci  4404  elsucg  4405  elsuc2g  4406  ordsucim  4500  peano2  4595  elxp  4644  brab2a  4680  brab2ga  4702  elco  4794  elcnv  4805  dmmrnm  4847  elrnmptg  4880  opelres  4913  rninxp  5073  eliota  5205  funco  5257  elfv  5514  nfvres  5549  fvopab3g  5590  fvmptssdm  5601  fmptco  5683  funfvima  5749  fliftel  5794  acexmidlema  5866  acexmidlemb  5867  acexmidlem2  5872  eloprabga  5962  elrnmpo  5988  ovid  5991  offval  6090  xporderlem  6232  brtpos2  6252  issmo  6289  smores3  6294  tfrlem7  6318  tfrlem9  6320  tfr0dm  6323  tfri2  6367  rdgon  6387  freccllem  6403  frecfcllem  6405  frecsuclem  6407  el1o  6438  dif1o  6439  nnsucuniel  6496  elecg  6573  brecop  6625  erovlem  6627  oviec  6641  mapsncnv  6695  mptelixpg  6734  isfi  6761  enssdom  6762  map1  6812  xpcomco  6826  exmidpw  6908  exmidpweq  6909  fnfi  6936  fidcenumlemrks  6952  fidcenumlemrk  6953  djulclb  7054  eldju  7067  eldju2ndl  7071  eldju2ndr  7072  ctssdccl  7110  pw1nel3  7230  sucpw1nel3  7232  elni  7307  nlt1pig  7340  0nnq  7363  dfmq0qs  7428  dfplq0qs  7429  nqnq0  7440  elinp  7473  0npr  7482  ltdfpr  7505  nqprl  7550  nqpru  7551  addnqprlemfl  7558  addnqprlemfu  7559  mulnqprlemfl  7574  mulnqprlemfu  7575  cauappcvgprlemladdru  7655  suplocexprlemell  7712  addsrpr  7744  mulsrpr  7745  opelcn  7825  opelreal  7826  elreal  7827  elreal2  7829  0ncn  7830  addcnsr  7833  mulcnsr  7834  addvalex  7843  peano1nnnn  7851  peano2nnnn  7852  xrlenlt  8022  1nn  8930  peano2nn  8931  elnn0  9178  elnnne0  9190  un0addcl  9209  un0mulcl  9210  elxnn0  9241  uztrn2  9545  elnnuz  9564  elnn0uz  9565  elq  9622  elxr  9776  elfzm1b  10098  fz01or  10111  frecfzennn  10426  inftonninf  10441  seqf  10461  ser0  10514  ser0f  10515  hashinfom  10758  clim2ser  11345  clim2ser2  11346  isermulc2  11348  iserle  11350  climserle  11353  fsum3cvg3  11404  isumclim3  11431  isumadd  11439  sumsplitdc  11440  iserabs  11483  cvgcmpub  11484  isumshft  11498  isumsplit  11499  isumlessdc  11504  cvgratz  11540  cvgratgt0  11541  clim2prod  11547  clim2divap  11548  prodf1  11550  zproddc  11587  prodsnf  11600  divides  11796  dvdsflip  11857  infssuzex  11950  ialgrlemconst  12043  prm23lt5  12263  4sqlem2  12387  ennnfonelemjn  12403  ennnfonelem1  12408  ennnfonelemdm  12421  basmex  12521  istps  13535  lmss  13749  txuni2  13759  sinq34lt0t  14255  lgsdir2lem2  14433  2sqlem1  14464  bdceq  14597  bj-nntrans  14706  bj-nnelirr  14708  ss1oel2o  14746  trilpolemisumle  14789