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  5638  nfvres  5676  fvopab3g  5720  fvmptssdm  5732  fmptco  5814  funfvima  5889  fliftel  5937  acexmidlema  6012  acexmidlemb  6013  acexmidlem2  6018  eloprabga  6111  elrnmpo  6138  ovid  6141  offval  6246  xporderlem  6399  brtpos2  6420  issmo  6457  smores3  6462  tfrlem7  6486  tfrlem9  6488  tfr0dm  6491  tfri2  6535  rdgon  6555  freccllem  6571  frecfcllem  6573  frecsuclem  6575  el1o  6608  dif1o  6609  nnsucuniel  6666  elecg  6745  brecop  6797  erovlem  6799  oviec  6813  mapsncnv  6867  mptelixpg  6906  isfi  6937  enssdom  6938  map1  6990  xpcomco  7013  exmidpw  7103  exmidpweq  7104  tpfidceq  7125  fnfi  7138  fidcenumlemrks  7155  fidcenumlemrk  7156  djulclb  7257  eldju  7270  eldju2ndl  7274  eldju2ndr  7275  ctssdccl  7313  pw1nel3  7452  sucpw1nel3  7454  elni  7531  nlt1pig  7564  0nnq  7587  dfmq0qs  7652  dfplq0qs  7653  nqnq0  7664  elinp  7697  0npr  7706  ltdfpr  7729  nqprl  7774  nqpru  7775  addnqprlemfl  7782  addnqprlemfu  7783  mulnqprlemfl  7798  mulnqprlemfu  7799  cauappcvgprlemladdru  7879  suplocexprlemell  7936  addsrpr  7968  mulsrpr  7969  opelcn  8049  opelreal  8050  elreal  8051  elreal2  8053  0ncn  8054  addcnsr  8057  mulcnsr  8058  addvalex  8067  peano1nnnn  8075  peano2nnnn  8076  xrlenlt  8247  1nn  9157  peano2nn  9158  elnn0  9407  elnnne0  9419  un0addcl  9438  un0mulcl  9439  elxnn0  9470  uztrn2  9777  elnnuz  9796  elnn0uz  9797  elq  9859  elxr  10014  elfzm1b  10336  fz01or  10349  infssuzex  10497  frecfzennn  10692  inftonninf  10708  seqf  10730  ser0  10799  ser0f  10800  hashinfom  11044  iswrd  11122  pfxccatpfx1  11324  clim2ser  11918  clim2ser2  11919  isermulc2  11921  iserle  11923  climserle  11926  fsum3cvg3  11978  isumclim3  12005  isumadd  12013  sumsplitdc  12014  iserabs  12057  cvgcmpub  12058  isumshft  12072  isumsplit  12073  isumlessdc  12078  cvgratz  12114  cvgratgt0  12115  clim2prod  12121  clim2divap  12122  prodf1  12124  zproddc  12161  prodsnf  12174  divides  12371  dvdsflip  12433  nninfctlemfo  12632  ialgrlemconst  12636  prm23lt5  12857  4sqlem2  12983  4sqlem12  12996  ennnfonelemjn  13044  ennnfonelem1  13049  ennnfonelemdm  13062  basmex  13163  ghmeqker  13879  isrhm  14194  rrgmex  14297  lssmex  14391  lidlmex  14511  2idlmex  14537  df2idl2  14545  2idlss  14550  psrbagf  14706  istps  14783  lmss  14997  txuni2  15007  dvply1  15516  sinq34lt0t  15582  lgsdir2lem2  15785  gausslemma2dlem1a  15814  lgsquadlem1  15833  lgsquadlem2  15834  2sqlem1  15870  isuhgrm  15949  isushgrm  15950  isupgren  15973  isumgren  15983  umgredg  16023  umgrpredgv  16025  umgredgne  16028  umgredgnlp  16030  isuspgren  16035  isusgren  16036  ausgrusgrien  16049  usgredgppren  16075  edgssv2en  16077  uspgredg2vlem  16098  uspgredg2v  16099  ushgredgedg  16104  ushgredgedgloop  16106  griedg0ssusgr  16129  uhgrissubgr  16139  subumgredg2en  16149  uhgrspansubgrlem  16154  vtxedgfi  16167  vtxlpfi  16168  vtxdg0v  16172  wlk1walkdom  16237  clwwlkccatlem  16278  clwwlknnn  16290  clwwlknon2x  16313  bdceq  16496  bj-nntrans  16605  bj-nnelirr  16607  ss1oel2o  16645  trilpolemisumle  16701