Theorem eleq2i 2145

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 2142	. 2 |- ( A = B -> ( C e. A <-> C e. B ) )
3	1, 2	ax-mp 7	1 |- ( C e. A <-> C e. B )

Syntax hints:   <-> wb 103   = wceq 1284   e. wcel 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077

This theorem is referenced by:  eleq12i  2146  eleqtri  2153  eleq2s  2173  hbxfreq  2185  abeq2i  2189  abeq1i  2190  nfceqi  2215  raleqbii  2378  rexeqbii  2379  rabeq2i  2598  elab2g  2740  elrabf  2747  elrab3t  2748  elrab2  2751  cbvsbc  2842  elin2  3156  dfnul2  3253  noel  3255  rabn0m  3272  rabeq0  3274  eltpg  3438  tpid3g  3505  oprcl  3594  elunirab  3614  elintrab  3648  exss  3982  elop  3986  opm  3989  brabsb  4016  brabga  4019  pofun  4067  elsuci  4158  elsucg  4159  elsuc2g  4160  ordsucim  4244  peano2  4336  elxp  4380  brab2a  4411  brab2ga  4433  elcnv  4530  dmmrnm  4572  elrnmptg  4604  opelres  4635  rninxp  4784  funco  4960  elfv  5196  nfvres  5227  fvopab3g  5266  fvmptssdm  5276  fmptco  5351  funfvima  5411  fliftel  5453  acexmidlema  5523  acexmidlemb  5524  acexmidlem2  5529  eloprabga  5611  elrnmpt2  5634  ovid  5637  offval  5739  xporderlem  5872  brtpos2  5889  issmo  5926  smores3  5931  tfrlem7  5956  tfrlem9  5958  tfr0  5960  tfri2  5975  el1o  6043  dif1o  6044  elecg  6167  brecop  6219  erovlem  6221  oviec  6235  isfi  6264  enssdom  6265  xpcomco  6323  fnfi  6388  elni  6498  nlt1pig  6531  0nnq  6554  dfmq0qs  6619  dfplq0qs  6620  nqnq0  6631  elinp  6664  0npr  6673  ltdfpr  6696  nqprl  6741  nqpru  6742  addnqprlemfl  6749  addnqprlemfu  6750  mulnqprlemfl  6765  mulnqprlemfu  6766  cauappcvgprlemladdru  6846  addsrpr  6922  mulsrpr  6923  opelcn  6995  opelreal  6996  elreal  6997  elreal2  6999  0ncn  7000  addcnsr  7002  mulcnsr  7003  addvalex  7012  peano1nnnn  7020  peano2nnnn  7021  xrlenlt  7177  1nn  8050  peano2nn  8051  elnn0  8290  elnnne0  8302  un0addcl  8321  un0mulcl  8322  uztrn2  8636  elnnuz  8655  elnn0uz  8656  elq  8707  elxr  8850  elfzm1b  9115  frecfzennn  9419  iseqf  9444  iser0  9471  iser0f  9472  clim2iser  10175  clim2iser2  10176  iisermulc2  10178  iserile  10180  climserile  10183  divides  10197  dvdsflip  10251  fz01or  10278  infssuzex  10345  ialgrlemconst  10425  ialgrf  10427  bdceq  10633  bj-nntrans  10746  bj-nnelirr  10748