Theorem eleq2i 2263

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 2260	. 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 1364   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eleq12i  2264  eleqtri  2271  eleq2s  2291  hbxfreq  2303  abeq2i  2307  abeq1i  2308  nfceqi  2335  raleqbii  2509  rexeqbii  2510  rabeq2i  2760  elab2g  2911  elrabf  2918  elrab3t  2919  elrab2  2923  cbvsbcw  3017  cbvsbc  3018  csbcow  3095  elin2  3352  dfnul2  3453  noel  3455  rabn0m  3479  rabeq0  3481  eltpg  3668  tpid3g  3738  oprcl  3833  elunirab  3853  elintrab  3887  exss  4261  elop  4265  opm  4268  brabsb  4296  brabga  4299  pofun  4348  elsuci  4439  elsucg  4440  elsuc2g  4441  ordsucim  4537  peano2  4632  elxp  4681  brab2a  4717  brab2ga  4739  elco  4833  elcnv  4844  dmmrnm  4886  elrnmptg  4919  opelres  4952  rninxp  5114  eliota  5247  funco  5299  elfv  5559  nfvres  5595  fvopab3g  5637  fvmptssdm  5649  fmptco  5731  funfvima  5797  fliftel  5843  acexmidlema  5916  acexmidlemb  5917  acexmidlem2  5922  eloprabga  6013  elrnmpo  6040  ovid  6043  offval  6147  xporderlem  6298  brtpos2  6318  issmo  6355  smores3  6360  tfrlem7  6384  tfrlem9  6386  tfr0dm  6389  tfri2  6433  rdgon  6453  freccllem  6469  frecfcllem  6471  frecsuclem  6473  el1o  6504  dif1o  6505  nnsucuniel  6562  elecg  6641  brecop  6693  erovlem  6695  oviec  6709  mapsncnv  6763  mptelixpg  6802  isfi  6829  enssdom  6830  map1  6880  xpcomco  6894  exmidpw  6978  exmidpweq  6979  tpfidceq  7000  fnfi  7011  fidcenumlemrks  7028  fidcenumlemrk  7029  djulclb  7130  eldju  7143  eldju2ndl  7147  eldju2ndr  7148  ctssdccl  7186  pw1nel3  7314  sucpw1nel3  7316  elni  7392  nlt1pig  7425  0nnq  7448  dfmq0qs  7513  dfplq0qs  7514  nqnq0  7525  elinp  7558  0npr  7567  ltdfpr  7590  nqprl  7635  nqpru  7636  addnqprlemfl  7643  addnqprlemfu  7644  mulnqprlemfl  7659  mulnqprlemfu  7660  cauappcvgprlemladdru  7740  suplocexprlemell  7797  addsrpr  7829  mulsrpr  7830  opelcn  7910  opelreal  7911  elreal  7912  elreal2  7914  0ncn  7915  addcnsr  7918  mulcnsr  7919  addvalex  7928  peano1nnnn  7936  peano2nnnn  7937  xrlenlt  8108  1nn  9018  peano2nn  9019  elnn0  9268  elnnne0  9280  un0addcl  9299  un0mulcl  9300  elxnn0  9331  uztrn2  9636  elnnuz  9655  elnn0uz  9656  elq  9713  elxr  9868  elfzm1b  10190  fz01or  10203  infssuzex  10340  frecfzennn  10535  inftonninf  10551  seqf  10573  ser0  10642  ser0f  10643  hashinfom  10887  iswrd  10954  clim2ser  11519  clim2ser2  11520  isermulc2  11522  iserle  11524  climserle  11527  fsum3cvg3  11578  isumclim3  11605  isumadd  11613  sumsplitdc  11614  iserabs  11657  cvgcmpub  11658  isumshft  11672  isumsplit  11673  isumlessdc  11678  cvgratz  11714  cvgratgt0  11715  clim2prod  11721  clim2divap  11722  prodf1  11724  zproddc  11761  prodsnf  11774  divides  11971  dvdsflip  12033  nninfctlemfo  12232  ialgrlemconst  12236  prm23lt5  12457  4sqlem2  12583  4sqlem12  12596  ennnfonelemjn  12644  ennnfonelem1  12649  ennnfonelemdm  12662  basmex  12762  ghmeqker  13477  isrhm  13790  rrgmex  13893  lssmex  13987  lidlmex  14107  2idlmex  14133  df2idl2  14141  2idlss  14146  psrbagf  14300  istps  14352  lmss  14566  txuni2  14576  dvply1  15085  sinq34lt0t  15151  lgsdir2lem2  15354  gausslemma2dlem1a  15383  lgsquadlem1  15402  lgsquadlem2  15403  2sqlem1  15439  bdceq  15572  bj-nntrans  15681  bj-nnelirr  15683  ss1oel2o  15722  trilpolemisumle  15769