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  3351  dfnul2  3452  noel  3454  rabn0m  3478  rabeq0  3480  eltpg  3667  tpid3g  3737  oprcl  3832  elunirab  3852  elintrab  3886  exss  4260  elop  4264  opm  4267  brabsb  4295  brabga  4298  pofun  4347  elsuci  4438  elsucg  4439  elsuc2g  4440  ordsucim  4536  peano2  4631  elxp  4680  brab2a  4716  brab2ga  4738  elco  4832  elcnv  4843  dmmrnm  4885  elrnmptg  4918  opelres  4951  rninxp  5113  eliota  5246  funco  5298  elfv  5556  nfvres  5592  fvopab3g  5634  fvmptssdm  5646  fmptco  5728  funfvima  5794  fliftel  5840  acexmidlema  5913  acexmidlemb  5914  acexmidlem2  5919  eloprabga  6009  elrnmpo  6036  ovid  6039  offval  6143  xporderlem  6289  brtpos2  6309  issmo  6346  smores3  6351  tfrlem7  6375  tfrlem9  6377  tfr0dm  6380  tfri2  6424  rdgon  6444  freccllem  6460  frecfcllem  6462  frecsuclem  6464  el1o  6495  dif1o  6496  nnsucuniel  6553  elecg  6632  brecop  6684  erovlem  6686  oviec  6700  mapsncnv  6754  mptelixpg  6793  isfi  6820  enssdom  6821  map1  6871  xpcomco  6885  exmidpw  6969  exmidpweq  6970  tpfidceq  6991  fnfi  7002  fidcenumlemrks  7019  fidcenumlemrk  7020  djulclb  7121  eldju  7134  eldju2ndl  7138  eldju2ndr  7139  ctssdccl  7177  pw1nel3  7298  sucpw1nel3  7300  elni  7375  nlt1pig  7408  0nnq  7431  dfmq0qs  7496  dfplq0qs  7497  nqnq0  7508  elinp  7541  0npr  7550  ltdfpr  7573  nqprl  7618  nqpru  7619  addnqprlemfl  7626  addnqprlemfu  7627  mulnqprlemfl  7642  mulnqprlemfu  7643  cauappcvgprlemladdru  7723  suplocexprlemell  7780  addsrpr  7812  mulsrpr  7813  opelcn  7893  opelreal  7894  elreal  7895  elreal2  7897  0ncn  7898  addcnsr  7901  mulcnsr  7902  addvalex  7911  peano1nnnn  7919  peano2nnnn  7920  xrlenlt  8091  1nn  9001  peano2nn  9002  elnn0  9251  elnnne0  9263  un0addcl  9282  un0mulcl  9283  elxnn0  9314  uztrn2  9619  elnnuz  9638  elnn0uz  9639  elq  9696  elxr  9851  elfzm1b  10173  fz01or  10186  infssuzex  10323  frecfzennn  10518  inftonninf  10534  seqf  10556  ser0  10625  ser0f  10626  hashinfom  10870  iswrd  10937  clim2ser  11502  clim2ser2  11503  isermulc2  11505  iserle  11507  climserle  11510  fsum3cvg3  11561  isumclim3  11588  isumadd  11596  sumsplitdc  11597  iserabs  11640  cvgcmpub  11641  isumshft  11655  isumsplit  11656  isumlessdc  11661  cvgratz  11697  cvgratgt0  11698  clim2prod  11704  clim2divap  11705  prodf1  11707  zproddc  11744  prodsnf  11757  divides  11954  dvdsflip  12016  nninfctlemfo  12207  ialgrlemconst  12211  prm23lt5  12432  4sqlem2  12558  4sqlem12  12571  ennnfonelemjn  12619  ennnfonelem1  12624  ennnfonelemdm  12637  basmex  12737  ghmeqker  13401  isrhm  13714  rrgmex  13817  lssmex  13911  lidlmex  14031  2idlmex  14057  df2idl2  14065  2idlss  14070  psrbagf  14224  istps  14268  lmss  14482  txuni2  14492  dvply1  15001  sinq34lt0t  15067  lgsdir2lem2  15270  gausslemma2dlem1a  15299  lgsquadlem1  15318  lgsquadlem2  15319  2sqlem1  15355  bdceq  15488  bj-nntrans  15597  bj-nnelirr  15599  ss1oel2o  15638  trilpolemisumle  15682