Theorem eleq2i 2260

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 2257	. 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 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

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

This theorem is referenced by:  eleq12i  2261  eleqtri  2268  eleq2s  2288  hbxfreq  2300  abeq2i  2304  abeq1i  2305  nfceqi  2332  raleqbii  2506  rexeqbii  2507  rabeq2i  2757  elab2g  2907  elrabf  2914  elrab3t  2915  elrab2  2919  cbvsbcw  3013  cbvsbc  3014  csbcow  3091  elin2  3347  dfnul2  3448  noel  3450  rabn0m  3474  rabeq0  3476  eltpg  3663  tpid3g  3733  oprcl  3828  elunirab  3848  elintrab  3882  exss  4256  elop  4260  opm  4263  brabsb  4291  brabga  4294  pofun  4343  elsuci  4434  elsucg  4435  elsuc2g  4436  ordsucim  4532  peano2  4627  elxp  4676  brab2a  4712  brab2ga  4734  elco  4828  elcnv  4839  dmmrnm  4881  elrnmptg  4914  opelres  4947  rninxp  5109  eliota  5242  funco  5294  elfv  5552  nfvres  5588  fvopab3g  5630  fvmptssdm  5642  fmptco  5724  funfvima  5790  fliftel  5836  acexmidlema  5909  acexmidlemb  5910  acexmidlem2  5915  eloprabga  6005  elrnmpo  6032  ovid  6035  offval  6138  xporderlem  6284  brtpos2  6304  issmo  6341  smores3  6346  tfrlem7  6370  tfrlem9  6372  tfr0dm  6375  tfri2  6419  rdgon  6439  freccllem  6455  frecfcllem  6457  frecsuclem  6459  el1o  6490  dif1o  6491  nnsucuniel  6548  elecg  6627  brecop  6679  erovlem  6681  oviec  6695  mapsncnv  6749  mptelixpg  6788  isfi  6815  enssdom  6816  map1  6866  xpcomco  6880  exmidpw  6964  exmidpweq  6965  fnfi  6995  fidcenumlemrks  7012  fidcenumlemrk  7013  djulclb  7114  eldju  7127  eldju2ndl  7131  eldju2ndr  7132  ctssdccl  7170  pw1nel3  7291  sucpw1nel3  7293  elni  7368  nlt1pig  7401  0nnq  7424  dfmq0qs  7489  dfplq0qs  7490  nqnq0  7501  elinp  7534  0npr  7543  ltdfpr  7566  nqprl  7611  nqpru  7612  addnqprlemfl  7619  addnqprlemfu  7620  mulnqprlemfl  7635  mulnqprlemfu  7636  cauappcvgprlemladdru  7716  suplocexprlemell  7773  addsrpr  7805  mulsrpr  7806  opelcn  7886  opelreal  7887  elreal  7888  elreal2  7890  0ncn  7891  addcnsr  7894  mulcnsr  7895  addvalex  7904  peano1nnnn  7912  peano2nnnn  7913  xrlenlt  8084  1nn  8993  peano2nn  8994  elnn0  9242  elnnne0  9254  un0addcl  9273  un0mulcl  9274  elxnn0  9305  uztrn2  9610  elnnuz  9629  elnn0uz  9630  elq  9687  elxr  9842  elfzm1b  10164  fz01or  10177  frecfzennn  10497  inftonninf  10513  seqf  10535  ser0  10604  ser0f  10605  hashinfom  10849  iswrd  10916  clim2ser  11480  clim2ser2  11481  isermulc2  11483  iserle  11485  climserle  11488  fsum3cvg3  11539  isumclim3  11566  isumadd  11574  sumsplitdc  11575  iserabs  11618  cvgcmpub  11619  isumshft  11633  isumsplit  11634  isumlessdc  11639  cvgratz  11675  cvgratgt0  11676  clim2prod  11682  clim2divap  11683  prodf1  11685  zproddc  11722  prodsnf  11735  divides  11932  dvdsflip  11993  infssuzex  12086  nninfctlemfo  12177  ialgrlemconst  12181  prm23lt5  12401  4sqlem2  12527  4sqlem12  12540  ennnfonelemjn  12559  ennnfonelem1  12564  ennnfonelemdm  12577  basmex  12677  ghmeqker  13341  isrhm  13654  rrgmex  13757  lssmex  13851  lidlmex  13971  2idlmex  13997  df2idl2  14005  2idlss  14010  psrbagf  14156  istps  14200  lmss  14414  txuni2  14424  sinq34lt0t  14966  lgsdir2lem2  15145  gausslemma2dlem1a  15174  lgsquadlem1  15191  2sqlem1  15201  bdceq  15334  bj-nntrans  15443  bj-nnelirr  15445  ss1oel2o  15484  trilpolemisumle  15528