Theorem eleq2i 2301

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 2298	. 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 1398   e. 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  3740  tpid3g  3813  oprcl  3913  elunirab  3933  elintrab  3967  exss  4349  elop  4353  opm  4356  brabsb  4385  brabga  4388  pofun  4439  elsuci  4530  elsucg  4531  elsuc2g  4532  ordsucim  4628  peano2  4723  elxp  4772  brab2a  4809  brab2ga  4831  elco  4927  elcnv  4938  dmmrnm  4982  elrnmptg  5015  opelres  5049  rninxp  5212  eliota  5346  funco  5398  elfv  5674  nfvres  5712  fvopab3g  5756  fvmptssdm  5768  fmptco  5849  funfvima  5924  fliftel  5973  acexmidlema  6050  acexmidlemb  6051  acexmidlem2  6056  eloprabga  6149  elrnmpo  6176  ovid  6179  offval  6284  xporderlem  6441  brtpos2  6496  issmo  6533  smores3  6538  tfrlem7  6562  tfrlem9  6564  tfr0dm  6567  tfri2  6611  rdgon  6631  freccllem  6647  frecfcllem  6649  frecsuclem  6651  el1o  6684  dif1o  6685  nnsucuniel  6742  elecg  6821  brecop  6873  erovlem  6875  oviec  6889  mapsncnv  6944  mptelixpg  6983  isfi  7014  enssdom  7015  map1  7068  xpcomco  7091  exmidpw  7182  exmidpweq  7183  tpfidceq  7204  fnfi  7217  fidcenumlemrks  7237  fidcenumlemrk  7238  djulclb  7360  eldju  7373  eldju2ndl  7377  eldju2ndr  7378  ctssdccl  7416  pw1nel3  7555  sucpw1nel3  7557  elni  7640  nlt1pig  7673  0nnq  7696  dfmq0qs  7761  dfplq0qs  7762  nqnq0  7773  elinp  7806  0npr  7815  ltdfpr  7838  nqprl  7883  nqpru  7884  addnqprlemfl  7891  addnqprlemfu  7892  mulnqprlemfl  7907  mulnqprlemfu  7908  cauappcvgprlemladdru  7988  suplocexprlemell  8045  addsrpr  8077  mulsrpr  8078  opelcn  8158  opelreal  8159  elreal  8160  elreal2  8162  0ncn  8163  addcnsr  8166  mulcnsr  8167  addvalex  8176  peano1nnnn  8184  peano2nnnn  8185  xrlenlt  8355  1nn  9269  peano2nn  9270  elnn0  9519  elnnne0  9531  un0addcl  9550  un0mulcl  9551  elxnn0  9586  uztrn2  9894  elnnuz  9913  elnn0uz  9914  elq  9976  elxr  10132  elfzm1b  10458  fz01or  10471  infssuzex  10619  infssfzcldc  10622  infssfzledc  10623  frecfzennn  10816  inftonninf  10832  seqf  10854  ser0  10923  ser0f  10924  hashinfom  11170  iswrd  11255  pfxccatpfx1  11457  clim2ser  12052  clim2ser2  12053  isermulc2  12055  iserle  12057  climserle  12060  fsum3cvg3  12112  isumclim3  12139  isumadd  12147  sumsplitdc  12148  iserabs  12191  cvgcmpub  12192  isumshft  12206  isumsplit  12207  isumlessdc  12212  cvgratz  12248  cvgratgt0  12249  clim2prod  12255  clim2divap  12256  prodf1  12258  zproddc  12295  prodsnf  12308  divides  12505  dvdsflip  12567  nninfctlemfo  12766  ialgrlemconst  12770  prm23lt5  12991  4sqlem2  13117  4sqlem12  13130  ballotfilemfrcn0  13222  ballotfilem7  13228  ennnfonelemjn  13242  ennnfonelem1  13247  ennnfonelemdm  13260  basmex  13361  ghmeqker  14029  opprringb  14329  isrhm  14408  rrgmex  14512  lssmex  14634  lidlmex  14754  2idlmex  14780  df2idl2  14788  2idlss  14793  psrbagf  14949  istps  15028  lmss  15242  txuni2  15252  dvply1  15761  sinq34lt0t  15827  lgsdir2lem2  16033  gausslemma2dlem1a  16062  lgsquadlem1  16081  lgsquadlem2  16082  2sqlem1  16118  isuhgrm  16197  isushgrm  16198  isupgren  16221  isumgren  16231  umgredg  16271  umgrpredgv  16273  umgredgne  16276  umgredgnlp  16278  isuspgren  16283  isusgren  16284  ausgrusgrien  16297  usgredgppren  16323  edgssv2en  16325  uspgredg2vlem  16346  uspgredg2v  16347  ushgredgedg  16352  ushgredgedgloop  16354  griedg0ssusgr  16377  uhgrissubgr  16387  subumgredg2en  16397  uhgrspansubgrlem  16402  vtxedgfi  16415  vtxlpfi  16416  vtxdg0v  16420  wlk1walkdom  16485  clwwlkccatlem  16526  clwwlknnn  16538  clwwlknon2x  16561  bdceq  16753  bj-nntrans  16862  bj-nnelirr  16864  ss1oel2o  16902  trilpolemisumle  16963