Theorem eleq2i 2296

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

Syntax hints:   ↔ wb 105   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12i  2297  eleqtri  2304  eleq2s  2324  hbxfreq  2336  abeq2i  2340  abeq1i  2341  nfceqi  2368  raleqbii  2542  rexeqbii  2543  rabeq2i  2797  elab2g  2951  elrabf  2958  elrab3t  2959  elrab2  2963  cbvsbcw  3057  cbvsbc  3058  csbcow  3136  elin2  3393  dfnul2  3494  noel  3496  rabn0m  3520  rabeq0  3522  eltpg  3712  tpid3g  3785  oprcl  3884  elunirab  3904  elintrab  3938  exss  4317  elop  4321  opm  4324  brabsb  4353  brabga  4356  pofun  4407  elsuci  4498  elsucg  4499  elsuc2g  4500  ordsucim  4596  peano2  4691  elxp  4740  brab2a  4777  brab2ga  4799  elco  4894  elcnv  4905  dmmrnm  4949  elrnmptg  4982  opelres  5016  rninxp  5178  eliota  5312  funco  5364  elfv  5633  nfvres  5671  fvopab3g  5715  fvmptssdm  5727  fmptco  5809  funfvima  5881  fliftel  5929  acexmidlema  6004  acexmidlemb  6005  acexmidlem2  6010  eloprabga  6103  elrnmpo  6130  ovid  6133  offval  6238  xporderlem  6391  brtpos2  6412  issmo  6449  smores3  6454  tfrlem7  6478  tfrlem9  6480  tfr0dm  6483  tfri2  6527  rdgon  6547  freccllem  6563  frecfcllem  6565  frecsuclem  6567  el1o  6600  dif1o  6601  nnsucuniel  6658  elecg  6737  brecop  6789  erovlem  6791  oviec  6805  mapsncnv  6859  mptelixpg  6898  isfi  6929  enssdom  6930  map1  6982  xpcomco  7005  exmidpw  7093  exmidpweq  7094  tpfidceq  7115  fnfi  7126  fidcenumlemrks  7143  fidcenumlemrk  7144  djulclb  7245  eldju  7258  eldju2ndl  7262  eldju2ndr  7263  ctssdccl  7301  pw1nel3  7439  sucpw1nel3  7441  elni  7518  nlt1pig  7551  0nnq  7574  dfmq0qs  7639  dfplq0qs  7640  nqnq0  7651  elinp  7684  0npr  7693  ltdfpr  7716  nqprl  7761  nqpru  7762  addnqprlemfl  7769  addnqprlemfu  7770  mulnqprlemfl  7785  mulnqprlemfu  7786  cauappcvgprlemladdru  7866  suplocexprlemell  7923  addsrpr  7955  mulsrpr  7956  opelcn  8036  opelreal  8037  elreal  8038  elreal2  8040  0ncn  8041  addcnsr  8044  mulcnsr  8045  addvalex  8054  peano1nnnn  8062  peano2nnnn  8063  xrlenlt  8234  1nn  9144  peano2nn  9145  elnn0  9394  elnnne0  9406  un0addcl  9425  un0mulcl  9426  elxnn0  9457  uztrn2  9764  elnnuz  9783  elnn0uz  9784  elq  9846  elxr  10001  elfzm1b  10323  fz01or  10336  infssuzex  10483  frecfzennn  10678  inftonninf  10694  seqf  10716  ser0  10785  ser0f  10786  hashinfom  11030  iswrd  11105  pfxccatpfx1  11307  clim2ser  11888  clim2ser2  11889  isermulc2  11891  iserle  11893  climserle  11896  fsum3cvg3  11947  isumclim3  11974  isumadd  11982  sumsplitdc  11983  iserabs  12026  cvgcmpub  12027  isumshft  12041  isumsplit  12042  isumlessdc  12047  cvgratz  12083  cvgratgt0  12084  clim2prod  12090  clim2divap  12091  prodf1  12093  zproddc  12130  prodsnf  12143  divides  12340  dvdsflip  12402  nninfctlemfo  12601  ialgrlemconst  12605  prm23lt5  12826  4sqlem2  12952  4sqlem12  12965  ennnfonelemjn  13013  ennnfonelem1  13018  ennnfonelemdm  13031  basmex  13132  ghmeqker  13848  isrhm  14162  rrgmex  14265  lssmex  14359  lidlmex  14479  2idlmex  14505  df2idl2  14513  2idlss  14518  psrbagf  14674  istps  14746  lmss  14960  txuni2  14970  dvply1  15479  sinq34lt0t  15545  lgsdir2lem2  15748  gausslemma2dlem1a  15777  lgsquadlem1  15796  lgsquadlem2  15797  2sqlem1  15833  isuhgrm  15912  isushgrm  15913  isupgren  15936  isumgren  15946  umgredg  15984  umgrpredgv  15986  umgredgne  15989  umgredgnlp  15991  isuspgren  15996  isusgren  15997  ausgrusgrien  16010  usgredgppren  16036  edgssv2en  16038  uspgredg2vlem  16059  uspgredg2v  16060  ushgredgedg  16065  ushgredgedgloop  16067  griedg0ssusgr  16090  vtxedgfi  16095  vtxlpfi  16096  vtxdg0v  16100  wlk1walkdom  16156  clwwlkccatlem  16195  clwwlknnn  16207  clwwlknon2x  16230  bdceq  16373  bj-nntrans  16482  bj-nnelirr  16484  ss1oel2o  16522  trilpolemisumle  16578