Theorem eleq2i 2296

Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eleq1i.1	|- A = B

Assertion

Ref	Expression
eleq2i	|- ( C e. A <-> C e. B )

Proof of Theorem eleq2i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 |- A = B
2		eleq2 2293	. 2 |- ( A = B -> ( C e. A <-> C e. B ) )
3	1, 2	ax-mp 5	1 |- ( C e. A <-> C e. B )

Syntax hints:   <-> wb 105   = wceq 1395   e. 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  2796  elab2g  2950  elrabf  2957  elrab3t  2958  elrab2  2962  cbvsbcw  3056  cbvsbc  3057  csbcow  3135  elin2  3392  dfnul2  3493  noel  3495  rabn0m  3519  rabeq0  3521  eltpg  3711  tpid3g  3782  oprcl  3881  elunirab  3901  elintrab  3935  exss  4313  elop  4317  opm  4320  brabsb  4349  brabga  4352  pofun  4403  elsuci  4494  elsucg  4495  elsuc2g  4496  ordsucim  4592  peano2  4687  elxp  4736  brab2a  4772  brab2ga  4794  elco  4888  elcnv  4899  dmmrnm  4943  elrnmptg  4976  opelres  5010  rninxp  5172  eliota  5306  funco  5358  elfv  5627  nfvres  5665  fvopab3g  5709  fvmptssdm  5721  fmptco  5803  funfvima  5875  fliftel  5923  acexmidlema  5998  acexmidlemb  5999  acexmidlem2  6004  eloprabga  6097  elrnmpo  6124  ovid  6127  offval  6232  xporderlem  6383  brtpos2  6403  issmo  6440  smores3  6445  tfrlem7  6469  tfrlem9  6471  tfr0dm  6474  tfri2  6518  rdgon  6538  freccllem  6554  frecfcllem  6556  frecsuclem  6558  el1o  6591  dif1o  6592  nnsucuniel  6649  elecg  6728  brecop  6780  erovlem  6782  oviec  6796  mapsncnv  6850  mptelixpg  6889  isfi  6920  enssdom  6921  map1  6973  xpcomco  6993  exmidpw  7081  exmidpweq  7082  tpfidceq  7103  fnfi  7114  fidcenumlemrks  7131  fidcenumlemrk  7132  djulclb  7233  eldju  7246  eldju2ndl  7250  eldju2ndr  7251  ctssdccl  7289  pw1nel3  7427  sucpw1nel3  7429  elni  7506  nlt1pig  7539  0nnq  7562  dfmq0qs  7627  dfplq0qs  7628  nqnq0  7639  elinp  7672  0npr  7681  ltdfpr  7704  nqprl  7749  nqpru  7750  addnqprlemfl  7757  addnqprlemfu  7758  mulnqprlemfl  7773  mulnqprlemfu  7774  cauappcvgprlemladdru  7854  suplocexprlemell  7911  addsrpr  7943  mulsrpr  7944  opelcn  8024  opelreal  8025  elreal  8026  elreal2  8028  0ncn  8029  addcnsr  8032  mulcnsr  8033  addvalex  8042  peano1nnnn  8050  peano2nnnn  8051  xrlenlt  8222  1nn  9132  peano2nn  9133  elnn0  9382  elnnne0  9394  un0addcl  9413  un0mulcl  9414  elxnn0  9445  uztrn2  9752  elnnuz  9771  elnn0uz  9772  elq  9829  elxr  9984  elfzm1b  10306  fz01or  10319  infssuzex  10465  frecfzennn  10660  inftonninf  10676  seqf  10698  ser0  10767  ser0f  10768  hashinfom  11012  iswrd  11086  pfxccatpfx1  11284  clim2ser  11864  clim2ser2  11865  isermulc2  11867  iserle  11869  climserle  11872  fsum3cvg3  11923  isumclim3  11950  isumadd  11958  sumsplitdc  11959  iserabs  12002  cvgcmpub  12003  isumshft  12017  isumsplit  12018  isumlessdc  12023  cvgratz  12059  cvgratgt0  12060  clim2prod  12066  clim2divap  12067  prodf1  12069  zproddc  12106  prodsnf  12119  divides  12316  dvdsflip  12378  nninfctlemfo  12577  ialgrlemconst  12581  prm23lt5  12802  4sqlem2  12928  4sqlem12  12941  ennnfonelemjn  12989  ennnfonelem1  12994  ennnfonelemdm  13007  basmex  13108  ghmeqker  13824  isrhm  14138  rrgmex  14241  lssmex  14335  lidlmex  14455  2idlmex  14481  df2idl2  14489  2idlss  14494  psrbagf  14650  istps  14722  lmss  14936  txuni2  14946  dvply1  15455  sinq34lt0t  15521  lgsdir2lem2  15724  gausslemma2dlem1a  15753  lgsquadlem1  15772  lgsquadlem2  15773  2sqlem1  15809  isuhgrm  15887  isushgrm  15888  isupgren  15911  isumgren  15921  umgredg  15959  umgrpredgv  15961  umgredgne  15964  umgredgnlp  15966  isuspgren  15971  isusgren  15972  ausgrusgrien  15985  usgredgppren  16011  edgssv2en  16013  uspgredg2vlem  16034  uspgredg2v  16035  ushgredgedg  16040  ushgredgedgloop  16042  vtxedgfi  16049  vtxlpfi  16050  vtxdg0v  16054  wlk1walkdom  16105  clwwlkccatlem  16143  clwwlknnn  16155  bdceq  16288  bj-nntrans  16397  bj-nnelirr  16399  ss1oel2o  16438  trilpolemisumle  16494