Theorem eleq2i 2301

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

Syntax hints:   ↔ wb 105   = wceq 1398   ∈ wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  eleq12i  2302  eleqtri  2309  eleq2s  2329  hbxfreq  2341  abeq2i  2345  abeq1i  2346  nfceqi  2382  raleqbii  2556  rexeqbii  2557  reqabi  2722  rabeq2i  2812  elab2g  2967  elrabf  2974  elrab3t  2975  elrab2  2979  cbvsbcw  3073  cbvsbc  3074  csbcow  3152  elin2  3411  dfnul2  3514  noel  3516  rabn0m  3540  rabeq0  3542  eltpg  3739  tpid3g  3812  oprcl  3912  elunirab  3932  elintrab  3966  exss  4348  elop  4352  opm  4355  brabsb  4384  brabga  4387  pofun  4438  elsuci  4529  elsucg  4530  elsuc2g  4531  ordsucim  4627  peano2  4722  elxp  4771  brab2a  4808  brab2ga  4830  elco  4926  elcnv  4937  dmmrnm  4981  elrnmptg  5014  opelres  5048  rninxp  5211  eliota  5345  funco  5397  elfv  5673  nfvres  5711  fvopab3g  5755  fvmptssdm  5767  fmptco  5848  funfvima  5923  fliftel  5972  acexmidlema  6049  acexmidlemb  6050  acexmidlem2  6055  eloprabga  6148  elrnmpo  6175  ovid  6178  offval  6283  xporderlem  6440  brtpos2  6495  issmo  6532  smores3  6537  tfrlem7  6561  tfrlem9  6563  tfr0dm  6566  tfri2  6610  rdgon  6630  freccllem  6646  frecfcllem  6648  frecsuclem  6650  el1o  6683  dif1o  6684  nnsucuniel  6741  elecg  6820  brecop  6872  erovlem  6874  oviec  6888  mapsncnv  6943  mptelixpg  6982  isfi  7013  enssdom  7014  map1  7067  xpcomco  7090  exmidpw  7181  exmidpweq  7182  tpfidceq  7203  fnfi  7216  fidcenumlemrks  7236  fidcenumlemrk  7237  djulclb  7359  eldju  7372  eldju2ndl  7376  eldju2ndr  7377  ctssdccl  7415  pw1nel3  7554  sucpw1nel3  7556  elni  7639  nlt1pig  7672  0nnq  7695  dfmq0qs  7760  dfplq0qs  7761  nqnq0  7772  elinp  7805  0npr  7814  ltdfpr  7837  nqprl  7882  nqpru  7883  addnqprlemfl  7890  addnqprlemfu  7891  mulnqprlemfl  7906  mulnqprlemfu  7907  cauappcvgprlemladdru  7987  suplocexprlemell  8044  addsrpr  8076  mulsrpr  8077  opelcn  8157  opelreal  8158  elreal  8159  elreal2  8161  0ncn  8162  addcnsr  8165  mulcnsr  8166  addvalex  8175  peano1nnnn  8183  peano2nnnn  8184  xrlenlt  8354  1nn  9265  peano2nn  9266  elnn0  9515  elnnne0  9527  un0addcl  9546  un0mulcl  9547  elxnn0  9582  uztrn2  9890  elnnuz  9909  elnn0uz  9910  elq  9972  elxr  10128  elfzm1b  10454  fz01or  10467  infssuzex  10615  infssfzcldc  10618  infssfzledc  10619  frecfzennn  10812  inftonninf  10828  seqf  10850  ser0  10919  ser0f  10920  hashinfom  11166  iswrd  11251  pfxccatpfx1  11453  clim2ser  12047  clim2ser2  12048  isermulc2  12050  iserle  12052  climserle  12055  fsum3cvg3  12107  isumclim3  12134  isumadd  12142  sumsplitdc  12143  iserabs  12186  cvgcmpub  12187  isumshft  12201  isumsplit  12202  isumlessdc  12207  cvgratz  12243  cvgratgt0  12244  clim2prod  12250  clim2divap  12251  prodf1  12253  zproddc  12290  prodsnf  12303  divides  12500  dvdsflip  12562  nninfctlemfo  12761  ialgrlemconst  12765  prm23lt5  12986  4sqlem2  13112  4sqlem12  13125  ballotfilemfrcn0  13217  ballotfilem7  13223  ennnfonelemjn  13237  ennnfonelem1  13242  ennnfonelemdm  13255  basmex  13356  ghmeqker  14024  opprringb  14324  isrhm  14403  rrgmex  14507  lssmex  14629  lidlmex  14749  2idlmex  14775  df2idl2  14783  2idlss  14788  psrbagf  14944  istps  15023  lmss  15237  txuni2  15247  dvply1  15756  sinq34lt0t  15822  lgsdir2lem2  16028  gausslemma2dlem1a  16057  lgsquadlem1  16076  lgsquadlem2  16077  2sqlem1  16113  isuhgrm  16192  isushgrm  16193  isupgren  16216  isumgren  16226  umgredg  16266  umgrpredgv  16268  umgredgne  16271  umgredgnlp  16273  isuspgren  16278  isusgren  16279  ausgrusgrien  16292  usgredgppren  16318  edgssv2en  16320  uspgredg2vlem  16341  uspgredg2v  16342  ushgredgedg  16347  ushgredgedgloop  16349  griedg0ssusgr  16372  uhgrissubgr  16382  subumgredg2en  16392  uhgrspansubgrlem  16397  vtxedgfi  16410  vtxlpfi  16411  vtxdg0v  16415  wlk1walkdom  16480  clwwlkccatlem  16521  clwwlknnn  16533  clwwlknon2x  16556  bdceq  16738  bj-nntrans  16847  bj-nnelirr  16849  ss1oel2o  16887  trilpolemisumle  16948