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  2908  elrabf  2915  elrab3t  2916  elrab2  2920  cbvsbcw  3014  cbvsbc  3015  csbcow  3092  elin2  3348  dfnul2  3449  noel  3451  rabn0m  3475  rabeq0  3477  eltpg  3664  tpid3g  3734  oprcl  3829  elunirab  3849  elintrab  3883  exss  4257  elop  4261  opm  4264  brabsb  4292  brabga  4295  pofun  4344  elsuci  4435  elsucg  4436  elsuc2g  4437  ordsucim  4533  peano2  4628  elxp  4677  brab2a  4713  brab2ga  4735  elco  4829  elcnv  4840  dmmrnm  4882  elrnmptg  4915  opelres  4948  rninxp  5110  eliota  5243  funco  5295  elfv  5553  nfvres  5589  fvopab3g  5631  fvmptssdm  5643  fmptco  5725  funfvima  5791  fliftel  5837  acexmidlema  5910  acexmidlemb  5911  acexmidlem2  5916  eloprabga  6006  elrnmpo  6033  ovid  6036  offval  6140  xporderlem  6286  brtpos2  6306  issmo  6343  smores3  6348  tfrlem7  6372  tfrlem9  6374  tfr0dm  6377  tfri2  6421  rdgon  6441  freccllem  6457  frecfcllem  6459  frecsuclem  6461  el1o  6492  dif1o  6493  nnsucuniel  6550  elecg  6629  brecop  6681  erovlem  6683  oviec  6697  mapsncnv  6751  mptelixpg  6790  isfi  6817  enssdom  6818  map1  6868  xpcomco  6882  exmidpw  6966  exmidpweq  6967  fnfi  6997  fidcenumlemrks  7014  fidcenumlemrk  7015  djulclb  7116  eldju  7129  eldju2ndl  7133  eldju2ndr  7134  ctssdccl  7172  pw1nel3  7293  sucpw1nel3  7295  elni  7370  nlt1pig  7403  0nnq  7426  dfmq0qs  7491  dfplq0qs  7492  nqnq0  7503  elinp  7536  0npr  7545  ltdfpr  7568  nqprl  7613  nqpru  7614  addnqprlemfl  7621  addnqprlemfu  7622  mulnqprlemfl  7637  mulnqprlemfu  7638  cauappcvgprlemladdru  7718  suplocexprlemell  7775  addsrpr  7807  mulsrpr  7808  opelcn  7888  opelreal  7889  elreal  7890  elreal2  7892  0ncn  7893  addcnsr  7896  mulcnsr  7897  addvalex  7906  peano1nnnn  7914  peano2nnnn  7915  xrlenlt  8086  1nn  8995  peano2nn  8996  elnn0  9245  elnnne0  9257  un0addcl  9276  un0mulcl  9277  elxnn0  9308  uztrn2  9613  elnnuz  9632  elnn0uz  9633  elq  9690  elxr  9845  elfzm1b  10167  fz01or  10180  frecfzennn  10500  inftonninf  10516  seqf  10538  ser0  10607  ser0f  10608  hashinfom  10852  iswrd  10919  clim2ser  11483  clim2ser2  11484  isermulc2  11486  iserle  11488  climserle  11491  fsum3cvg3  11542  isumclim3  11569  isumadd  11577  sumsplitdc  11578  iserabs  11621  cvgcmpub  11622  isumshft  11636  isumsplit  11637  isumlessdc  11642  cvgratz  11678  cvgratgt0  11679  clim2prod  11685  clim2divap  11686  prodf1  11688  zproddc  11725  prodsnf  11738  divides  11935  dvdsflip  11996  infssuzex  12089  nninfctlemfo  12180  ialgrlemconst  12184  prm23lt5  12404  4sqlem2  12530  4sqlem12  12543  ennnfonelemjn  12562  ennnfonelem1  12567  ennnfonelemdm  12580  basmex  12680  ghmeqker  13344  isrhm  13657  rrgmex  13760  lssmex  13854  lidlmex  13974  2idlmex  14000  df2idl2  14008  2idlss  14013  psrbagf  14167  istps  14211  lmss  14425  txuni2  14435  dvply1  14943  sinq34lt0t  15007  lgsdir2lem2  15186  gausslemma2dlem1a  15215  lgsquadlem1  15234  lgsquadlem2  15235  2sqlem1  15271  bdceq  15404  bj-nntrans  15513  bj-nnelirr  15515  ss1oel2o  15554  trilpolemisumle  15598