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  4369  elop  4373  opm  4376  brabsb  4405  brabga  4408  pofun  4459  elsuci  4550  elsucg  4551  elsuc2g  4552  ordsucim  4649  peano2  4744  elxp  4793  brab2a  4830  brab2ga  4852  elco  4948  elcnv  4959  dmmrnm  5003  elrnmptg  5036  opelres  5070  rninxp  5234  eliota  5368  funco  5420  elfv  5696  nfvres  5735  fvopab3g  5781  fvmptssdm  5793  fmptco  5877  funfvima  5953  fliftel  6002  acexmidlema  6079  acexmidlemb  6080  acexmidlem2  6085  eloprabga  6178  elrnmpo  6205  ovid  6208  offval  6314  xporderlem  6471  brtpos2  6527  issmo  6564  smores3  6569  tfrlem7  6593  tfrlem9  6595  tfr0dm  6598  tfri2  6642  rdgon  6662  freccllem  6678  frecfcllem  6680  frecsuclem  6682  el1o  6715  dif1o  6716  nnsucuniel  6773  elecg  6852  brecop  6904  erovlem  6906  oviec  6920  mapsncnv  6983  mptelixpg  7022  isfi  7053  enssdom  7054  map1  7107  xpcomco  7130  exmidpw  7221  exmidpweq  7222  tpfidceq  7243  fnfi  7256  fidcenumlemrks  7277  fidcenumlemrk  7278  djulclb  7401  eldju  7414  eldju2ndl  7418  eldju2ndr  7419  ctssdccl  7457  pw1nel3  7596  sucpw1nel3  7598  elni  7681  nlt1pig  7714  0nnq  7737  dfmq0qs  7802  dfplq0qs  7803  nqnq0  7814  elinp  7847  0npr  7856  ltdfpr  7879  nqprl  7924  nqpru  7925  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemfl  7948  mulnqprlemfu  7949  cauappcvgprlemladdru  8029  suplocexprlemell  8086  addsrpr  8118  mulsrpr  8119  opelcn  8199  opelreal  8200  elreal  8201  elreal2  8203  0ncn  8204  addcnsr  8207  mulcnsr  8208  addvalex  8217  peano1nnnn  8225  peano2nnnn  8226  xrlenlt  8396  1nn  9324  peano2nn  9325  elnn0  9576  elnnne0  9588  un0addcl  9607  un0mulcl  9608  elxnn0  9641  uztrn2  9955  elnnuz  9974  elnn0uz  9975  elq  10037  elxr  10194  elfzm1b  10521  fz01or  10534  infssuzex  10682  infssfzcldc  10685  infssfzledc  10686  frecfzennn  10883  inftonninf  10899  seqf  10921  ser0  10990  ser0f  10991  hashinfom  11238  iswrd  11327  pfxccatpfx1  11529  clim2ser  12127  clim2ser2  12128  isermulc2  12130  iserle  12132  climserle  12135  fsum3cvg3  12187  isumclim3  12214  isumadd  12222  sumsplitdc  12223  iserabs  12266  cvgcmpub  12267  isumshft  12281  isumsplit  12282  isumlessdc  12287  cvgratz  12323  cvgratgt0  12324  clim2prod  12330  clim2divap  12331  prodf1  12333  zproddc  12370  prodsnf  12383  divides  12580  dvdsflip  12642  nninfctlemfo  12841  ialgrlemconst  12845  prm23lt5  13070  4sqlem2  13196  4sqlem12  13209  ballotfilemfrcn0  13330  ballotfilem7  13336  ennnfonelemjn  13350  ennnfonelem1  13355  ennnfonelemdm  13368  basmex  13469  ghmeqker  14132  elcntr  14162  cntri  14164  cntzsgrpcl  14166  idjusnfi  14269  opprringb  14494  isrhm  14573  rrgmex  14677  lssmex  14800  lidlmex  14920  2idlmex  14946  df2idl2  14954  2idlss  14959  psrbagf  15164  istps  15275  lmss  15489  txuni2  15499  dvply1  16008  sinq34lt0t  16075  logfac  16143  ppiublem1  16308  lgsdir2lem2  16370  gausslemma2dlem1a  16399  lgsquadlem1  16418  lgsquadlem2  16419  2sqlem1  16455  isuhgrm  16534  isushgrm  16535  isupgren  16558  isumgren  16568  umgredg  16608  umgrpredgv  16610  umgredgne  16613  umgredgnlp  16615  isuspgren  16620  isusgren  16621  ausgrusgrien  16634  usgredgppren  16660  edgssv2en  16662  uspgredg2vlem  16683  uspgredg2v  16684  ushgredgedg  16689  ushgredgedgloop  16691  griedg0ssusgr  16714  uhgrissubgr  16724  subumgredg2en  16734  uhgrspansubgrlem  16739  vtxedgfi  16752  vtxlpfi  16753  vtxdg0v  16757  wlk1walkdom  16822  clwwlkccatlem  16863  clwwlknnn  16875  clwwlknon2x  16898  bdceq  17090  bj-nntrans  17199  bj-nnelirr  17201  ss1oel2o  17239  wexmiddifxylem  17267  idjudju  17269  trilpolemisumle  17311