Theorem eleq2i 2298

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 2295	. 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 1397   e. wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

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

This theorem is referenced by:  eleq12i  2299  eleqtri  2306  eleq2s  2326  hbxfreq  2338  abeq2i  2342  abeq1i  2343  nfceqi  2370  raleqbii  2544  rexeqbii  2545  rabeq2i  2799  elab2g  2953  elrabf  2960  elrab3t  2961  elrab2  2965  cbvsbcw  3059  cbvsbc  3060  csbcow  3138  elin2  3395  dfnul2  3496  noel  3498  rabn0m  3522  rabeq0  3524  eltpg  3714  tpid3g  3787  oprcl  3886  elunirab  3906  elintrab  3940  exss  4319  elop  4323  opm  4326  brabsb  4355  brabga  4358  pofun  4409  elsuci  4500  elsucg  4501  elsuc2g  4502  ordsucim  4598  peano2  4693  elxp  4742  brab2a  4779  brab2ga  4801  elco  4896  elcnv  4907  dmmrnm  4951  elrnmptg  4984  opelres  5018  rninxp  5180  eliota  5314  funco  5366  elfv  5637  nfvres  5675  fvopab3g  5719  fvmptssdm  5731  fmptco  5813  funfvima  5886  fliftel  5934  acexmidlema  6009  acexmidlemb  6010  acexmidlem2  6015  eloprabga  6108  elrnmpo  6135  ovid  6138  offval  6243  xporderlem  6396  brtpos2  6417  issmo  6454  smores3  6459  tfrlem7  6483  tfrlem9  6485  tfr0dm  6488  tfri2  6532  rdgon  6552  freccllem  6568  frecfcllem  6570  frecsuclem  6572  el1o  6605  dif1o  6606  nnsucuniel  6663  elecg  6742  brecop  6794  erovlem  6796  oviec  6810  mapsncnv  6864  mptelixpg  6903  isfi  6934  enssdom  6935  map1  6987  xpcomco  7010  exmidpw  7100  exmidpweq  7101  tpfidceq  7122  fnfi  7135  fidcenumlemrks  7152  fidcenumlemrk  7153  djulclb  7254  eldju  7267  eldju2ndl  7271  eldju2ndr  7272  ctssdccl  7310  pw1nel3  7449  sucpw1nel3  7451  elni  7528  nlt1pig  7561  0nnq  7584  dfmq0qs  7649  dfplq0qs  7650  nqnq0  7661  elinp  7694  0npr  7703  ltdfpr  7726  nqprl  7771  nqpru  7772  addnqprlemfl  7779  addnqprlemfu  7780  mulnqprlemfl  7795  mulnqprlemfu  7796  cauappcvgprlemladdru  7876  suplocexprlemell  7933  addsrpr  7965  mulsrpr  7966  opelcn  8046  opelreal  8047  elreal  8048  elreal2  8050  0ncn  8051  addcnsr  8054  mulcnsr  8055  addvalex  8064  peano1nnnn  8072  peano2nnnn  8073  xrlenlt  8244  1nn  9154  peano2nn  9155  elnn0  9404  elnnne0  9416  un0addcl  9435  un0mulcl  9436  elxnn0  9467  uztrn2  9774  elnnuz  9793  elnn0uz  9794  elq  9856  elxr  10011  elfzm1b  10333  fz01or  10346  infssuzex  10494  frecfzennn  10689  inftonninf  10705  seqf  10727  ser0  10796  ser0f  10797  hashinfom  11041  iswrd  11116  pfxccatpfx1  11318  clim2ser  11899  clim2ser2  11900  isermulc2  11902  iserle  11904  climserle  11907  fsum3cvg3  11959  isumclim3  11986  isumadd  11994  sumsplitdc  11995  iserabs  12038  cvgcmpub  12039  isumshft  12053  isumsplit  12054  isumlessdc  12059  cvgratz  12095  cvgratgt0  12096  clim2prod  12102  clim2divap  12103  prodf1  12105  zproddc  12142  prodsnf  12155  divides  12352  dvdsflip  12414  nninfctlemfo  12613  ialgrlemconst  12617  prm23lt5  12838  4sqlem2  12964  4sqlem12  12977  ennnfonelemjn  13025  ennnfonelem1  13030  ennnfonelemdm  13043  basmex  13144  ghmeqker  13860  isrhm  14175  rrgmex  14278  lssmex  14372  lidlmex  14492  2idlmex  14518  df2idl2  14526  2idlss  14531  psrbagf  14687  istps  14759  lmss  14973  txuni2  14983  dvply1  15492  sinq34lt0t  15558  lgsdir2lem2  15761  gausslemma2dlem1a  15790  lgsquadlem1  15809  lgsquadlem2  15810  2sqlem1  15846  isuhgrm  15925  isushgrm  15926  isupgren  15949  isumgren  15959  umgredg  15999  umgrpredgv  16001  umgredgne  16004  umgredgnlp  16006  isuspgren  16011  isusgren  16012  ausgrusgrien  16025  usgredgppren  16051  edgssv2en  16053  uspgredg2vlem  16074  uspgredg2v  16075  ushgredgedg  16080  ushgredgedgloop  16082  griedg0ssusgr  16105  uhgrissubgr  16115  subumgredg2en  16125  uhgrspansubgrlem  16130  vtxedgfi  16143  vtxlpfi  16144  vtxdg0v  16148  wlk1walkdom  16213  clwwlkccatlem  16254  clwwlknnn  16266  clwwlknon2x  16289  bdceq  16454  bj-nntrans  16563  bj-nnelirr  16565  ss1oel2o  16603  trilpolemisumle  16659