Theorem eleq2i 2274

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 2271	. 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 1373   e. wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  eleq12i  2275  eleqtri  2282  eleq2s  2302  hbxfreq  2314  abeq2i  2318  abeq1i  2319  nfceqi  2346  raleqbii  2520  rexeqbii  2521  rabeq2i  2773  elab2g  2927  elrabf  2934  elrab3t  2935  elrab2  2939  cbvsbcw  3033  cbvsbc  3034  csbcow  3112  elin2  3369  dfnul2  3470  noel  3472  rabn0m  3496  rabeq0  3498  eltpg  3688  tpid3g  3758  oprcl  3857  elunirab  3877  elintrab  3911  exss  4289  elop  4293  opm  4296  brabsb  4325  brabga  4328  pofun  4377  elsuci  4468  elsucg  4469  elsuc2g  4470  ordsucim  4566  peano2  4661  elxp  4710  brab2a  4746  brab2ga  4768  elco  4862  elcnv  4873  dmmrnm  4916  elrnmptg  4949  opelres  4983  rninxp  5145  eliota  5278  funco  5330  elfv  5597  nfvres  5633  fvopab3g  5675  fvmptssdm  5687  fmptco  5769  funfvima  5839  fliftel  5885  acexmidlema  5958  acexmidlemb  5959  acexmidlem2  5964  eloprabga  6055  elrnmpo  6082  ovid  6085  offval  6189  xporderlem  6340  brtpos2  6360  issmo  6397  smores3  6402  tfrlem7  6426  tfrlem9  6428  tfr0dm  6431  tfri2  6475  rdgon  6495  freccllem  6511  frecfcllem  6513  frecsuclem  6515  el1o  6546  dif1o  6547  nnsucuniel  6604  elecg  6683  brecop  6735  erovlem  6737  oviec  6751  mapsncnv  6805  mptelixpg  6844  isfi  6875  enssdom  6876  map1  6928  xpcomco  6946  exmidpw  7031  exmidpweq  7032  tpfidceq  7053  fnfi  7064  fidcenumlemrks  7081  fidcenumlemrk  7082  djulclb  7183  eldju  7196  eldju2ndl  7200  eldju2ndr  7201  ctssdccl  7239  pw1nel3  7377  sucpw1nel3  7379  elni  7456  nlt1pig  7489  0nnq  7512  dfmq0qs  7577  dfplq0qs  7578  nqnq0  7589  elinp  7622  0npr  7631  ltdfpr  7654  nqprl  7699  nqpru  7700  addnqprlemfl  7707  addnqprlemfu  7708  mulnqprlemfl  7723  mulnqprlemfu  7724  cauappcvgprlemladdru  7804  suplocexprlemell  7861  addsrpr  7893  mulsrpr  7894  opelcn  7974  opelreal  7975  elreal  7976  elreal2  7978  0ncn  7979  addcnsr  7982  mulcnsr  7983  addvalex  7992  peano1nnnn  8000  peano2nnnn  8001  xrlenlt  8172  1nn  9082  peano2nn  9083  elnn0  9332  elnnne0  9344  un0addcl  9363  un0mulcl  9364  elxnn0  9395  uztrn2  9701  elnnuz  9720  elnn0uz  9721  elq  9778  elxr  9933  elfzm1b  10255  fz01or  10268  infssuzex  10413  frecfzennn  10608  inftonninf  10624  seqf  10646  ser0  10715  ser0f  10716  hashinfom  10960  iswrd  11033  pfxccatpfx1  11227  clim2ser  11763  clim2ser2  11764  isermulc2  11766  iserle  11768  climserle  11771  fsum3cvg3  11822  isumclim3  11849  isumadd  11857  sumsplitdc  11858  iserabs  11901  cvgcmpub  11902  isumshft  11916  isumsplit  11917  isumlessdc  11922  cvgratz  11958  cvgratgt0  11959  clim2prod  11965  clim2divap  11966  prodf1  11968  zproddc  12005  prodsnf  12018  divides  12215  dvdsflip  12277  nninfctlemfo  12476  ialgrlemconst  12480  prm23lt5  12701  4sqlem2  12827  4sqlem12  12840  ennnfonelemjn  12888  ennnfonelem1  12893  ennnfonelemdm  12906  basmex  13006  ghmeqker  13722  isrhm  14035  rrgmex  14138  lssmex  14232  lidlmex  14352  2idlmex  14378  df2idl2  14386  2idlss  14391  psrbagf  14547  istps  14619  lmss  14833  txuni2  14843  dvply1  15352  sinq34lt0t  15418  lgsdir2lem2  15621  gausslemma2dlem1a  15650  lgsquadlem1  15669  lgsquadlem2  15670  2sqlem1  15706  isuhgrm  15782  isushgrm  15783  isupgren  15806  isumgren  15816  umgredg  15849  umgrpredgv  15851  umgredgne  15854  umgredgnlp  15856  bdceq  15977  bj-nntrans  16086  bj-nnelirr  16088  ss1oel2o  16127  trilpolemisumle  16179