Theorem eleq2i 2272

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 2269	. 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 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eleq12i  2273  eleqtri  2280  eleq2s  2300  hbxfreq  2312  abeq2i  2316  abeq1i  2317  nfceqi  2344  raleqbii  2518  rexeqbii  2519  rabeq2i  2769  elab2g  2920  elrabf  2927  elrab3t  2928  elrab2  2932  cbvsbcw  3026  cbvsbc  3027  csbcow  3104  elin2  3361  dfnul2  3462  noel  3464  rabn0m  3488  rabeq0  3490  eltpg  3678  tpid3g  3748  oprcl  3843  elunirab  3863  elintrab  3897  exss  4272  elop  4276  opm  4279  brabsb  4308  brabga  4311  pofun  4360  elsuci  4451  elsucg  4452  elsuc2g  4453  ordsucim  4549  peano2  4644  elxp  4693  brab2a  4729  brab2ga  4751  elco  4845  elcnv  4856  dmmrnm  4898  elrnmptg  4931  opelres  4965  rninxp  5127  eliota  5260  funco  5312  elfv  5576  nfvres  5612  fvopab3g  5654  fvmptssdm  5666  fmptco  5748  funfvima  5818  fliftel  5864  acexmidlema  5937  acexmidlemb  5938  acexmidlem2  5943  eloprabga  6034  elrnmpo  6061  ovid  6064  offval  6168  xporderlem  6319  brtpos2  6339  issmo  6376  smores3  6381  tfrlem7  6405  tfrlem9  6407  tfr0dm  6410  tfri2  6454  rdgon  6474  freccllem  6490  frecfcllem  6492  frecsuclem  6494  el1o  6525  dif1o  6526  nnsucuniel  6583  elecg  6662  brecop  6714  erovlem  6716  oviec  6730  mapsncnv  6784  mptelixpg  6823  isfi  6854  enssdom  6855  map1  6906  xpcomco  6923  exmidpw  7007  exmidpweq  7008  tpfidceq  7029  fnfi  7040  fidcenumlemrks  7057  fidcenumlemrk  7058  djulclb  7159  eldju  7172  eldju2ndl  7176  eldju2ndr  7177  ctssdccl  7215  pw1nel3  7345  sucpw1nel3  7347  elni  7423  nlt1pig  7456  0nnq  7479  dfmq0qs  7544  dfplq0qs  7545  nqnq0  7556  elinp  7589  0npr  7598  ltdfpr  7621  nqprl  7666  nqpru  7667  addnqprlemfl  7674  addnqprlemfu  7675  mulnqprlemfl  7690  mulnqprlemfu  7691  cauappcvgprlemladdru  7771  suplocexprlemell  7828  addsrpr  7860  mulsrpr  7861  opelcn  7941  opelreal  7942  elreal  7943  elreal2  7945  0ncn  7946  addcnsr  7949  mulcnsr  7950  addvalex  7959  peano1nnnn  7967  peano2nnnn  7968  xrlenlt  8139  1nn  9049  peano2nn  9050  elnn0  9299  elnnne0  9311  un0addcl  9330  un0mulcl  9331  elxnn0  9362  uztrn2  9668  elnnuz  9687  elnn0uz  9688  elq  9745  elxr  9900  elfzm1b  10222  fz01or  10235  infssuzex  10378  frecfzennn  10573  inftonninf  10589  seqf  10611  ser0  10680  ser0f  10681  hashinfom  10925  iswrd  10998  clim2ser  11681  clim2ser2  11682  isermulc2  11684  iserle  11686  climserle  11689  fsum3cvg3  11740  isumclim3  11767  isumadd  11775  sumsplitdc  11776  iserabs  11819  cvgcmpub  11820  isumshft  11834  isumsplit  11835  isumlessdc  11840  cvgratz  11876  cvgratgt0  11877  clim2prod  11883  clim2divap  11884  prodf1  11886  zproddc  11923  prodsnf  11936  divides  12133  dvdsflip  12195  nninfctlemfo  12394  ialgrlemconst  12398  prm23lt5  12619  4sqlem2  12745  4sqlem12  12758  ennnfonelemjn  12806  ennnfonelem1  12811  ennnfonelemdm  12824  basmex  12924  ghmeqker  13640  isrhm  13953  rrgmex  14056  lssmex  14150  lidlmex  14270  2idlmex  14296  df2idl2  14304  2idlss  14309  psrbagf  14465  istps  14537  lmss  14751  txuni2  14761  dvply1  15270  sinq34lt0t  15336  lgsdir2lem2  15539  gausslemma2dlem1a  15568  lgsquadlem1  15587  lgsquadlem2  15588  2sqlem1  15624  bdceq  15815  bj-nntrans  15924  bj-nnelirr  15926  ss1oel2o  15965  trilpolemisumle  16014