Theorem eleq2i 2305

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 2302	. 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 1402   e. wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  eleq12i  2306  eleqtri  2313  eleq2s  2333  hbxfreq  2345  abeq2i  2349  abeq1i  2350  nfceqi  2388  raleqbii  2562  rexeqbii  2563  reqabi  2728  rabeq2i  2818  elab2g  2973  elrabf  2980  elrab3t  2981  elrab2  2985  cbvsbcw  3079  cbvsbc  3080  csbcow  3158  elin2  3417  noel  3525  rabn0m  3549  rabeq0  3552  eltpg  3753  tpid3g  3826  oprcl  3926  elunirab  3946  elintrab  3980  exss  4365  elop  4369  opm  4372  brabsb  4401  brabga  4404  pofun  4455  elsuci  4546  elsucg  4547  elsuc2g  4548  ordsucim  4645  peano2  4740  elxp  4789  brab2a  4826  brab2ga  4848  elco  4944  elcnv  4955  dmmrnm  4999  elrnmptg  5032  opelres  5066  rninxp  5229  eliota  5363  funco  5415  elfv  5691  nfvres  5729  fvopab3g  5775  fvmptssdm  5787  fmptco  5868  funfvima  5944  fliftel  5993  acexmidlema  6070  acexmidlemb  6071  acexmidlem2  6076  eloprabga  6169  elrnmpo  6196  ovid  6199  offval  6304  xporderlem  6461  brtpos2  6516  issmo  6553  smores3  6558  tfrlem7  6582  tfrlem9  6584  tfr0dm  6587  tfri2  6631  rdgon  6651  freccllem  6667  frecfcllem  6669  frecsuclem  6671  el1o  6704  dif1o  6705  nnsucuniel  6762  elecg  6841  brecop  6893  erovlem  6895  oviec  6909  mapsncnv  6971  mptelixpg  7010  isfi  7041  enssdom  7042  map1  7095  xpcomco  7118  exmidpw  7209  exmidpweq  7210  tpfidceq  7231  fnfi  7244  fidcenumlemrks  7264  fidcenumlemrk  7265  djulclb  7389  eldju  7402  eldju2ndl  7406  eldju2ndr  7407  ctssdccl  7445  pw1nel3  7584  sucpw1nel3  7586  elni  7669  nlt1pig  7702  0nnq  7725  dfmq0qs  7790  dfplq0qs  7791  nqnq0  7802  elinp  7835  0npr  7844  ltdfpr  7867  nqprl  7912  nqpru  7913  addnqprlemfl  7920  addnqprlemfu  7921  mulnqprlemfl  7936  mulnqprlemfu  7937  cauappcvgprlemladdru  8017  suplocexprlemell  8074  addsrpr  8106  mulsrpr  8107  opelcn  8187  opelreal  8188  elreal  8189  elreal2  8191  0ncn  8192  addcnsr  8195  mulcnsr  8196  addvalex  8205  peano1nnnn  8213  peano2nnnn  8214  xrlenlt  8384  1nn  9298  peano2nn  9299  elnn0  9548  elnnne0  9560  un0addcl  9579  un0mulcl  9580  elxnn0  9615  uztrn2  9923  elnnuz  9942  elnn0uz  9943  elq  10005  elxr  10161  elfzm1b  10488  fz01or  10501  infssuzex  10649  infssfzcldc  10652  infssfzledc  10653  frecfzennn  10846  inftonninf  10862  seqf  10884  ser0  10953  ser0f  10954  hashinfom  11200  iswrd  11289  pfxccatpfx1  11491  clim2ser  12086  clim2ser2  12087  isermulc2  12089  iserle  12091  climserle  12094  fsum3cvg3  12146  isumclim3  12173  isumadd  12181  sumsplitdc  12182  iserabs  12225  cvgcmpub  12226  isumshft  12240  isumsplit  12241  isumlessdc  12246  cvgratz  12282  cvgratgt0  12283  clim2prod  12289  clim2divap  12290  prodf1  12292  zproddc  12329  prodsnf  12342  divides  12539  dvdsflip  12601  nninfctlemfo  12800  ialgrlemconst  12804  prm23lt5  13025  4sqlem2  13151  4sqlem12  13164  ballotfilemfrcn0  13256  ballotfilem7  13262  ennnfonelemjn  13276  ennnfonelem1  13281  ennnfonelemdm  13294  basmex  13395  ghmeqker  14057  opprringb  14369  isrhm  14448  rrgmex  14552  lssmex  14675  lidlmex  14795  2idlmex  14821  df2idl2  14829  2idlss  14834  psrbagf  15037  istps  15116  lmss  15330  txuni2  15340  dvply1  15849  sinq34lt0t  15915  logfac  15978  lgsdir2lem2  16131  gausslemma2dlem1a  16160  lgsquadlem1  16179  lgsquadlem2  16180  2sqlem1  16216  isuhgrm  16295  isushgrm  16296  isupgren  16319  isumgren  16329  umgredg  16369  umgrpredgv  16371  umgredgne  16374  umgredgnlp  16376  isuspgren  16381  isusgren  16382  ausgrusgrien  16395  usgredgppren  16421  edgssv2en  16423  uspgredg2vlem  16444  uspgredg2v  16445  ushgredgedg  16450  ushgredgedgloop  16452  griedg0ssusgr  16475  uhgrissubgr  16485  subumgredg2en  16495  uhgrspansubgrlem  16500  vtxedgfi  16513  vtxlpfi  16514  vtxdg0v  16518  wlk1walkdom  16583  clwwlkccatlem  16624  clwwlknnn  16636  clwwlknon2x  16659  bdceq  16851  bj-nntrans  16960  bj-nnelirr  16962  ss1oel2o  17000  trilpolemisumle  17061