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  4271  elop  4275  opm  4278  brabsb  4307  brabga  4310  pofun  4359  elsuci  4450  elsucg  4451  elsuc2g  4452  ordsucim  4548  peano2  4643  elxp  4692  brab2a  4728  brab2ga  4750  elco  4844  elcnv  4855  dmmrnm  4897  elrnmptg  4930  opelres  4964  rninxp  5126  eliota  5259  funco  5311  elfv  5574  nfvres  5610  fvopab3g  5652  fvmptssdm  5664  fmptco  5746  funfvima  5816  fliftel  5862  acexmidlema  5935  acexmidlemb  5936  acexmidlem2  5941  eloprabga  6032  elrnmpo  6059  ovid  6062  offval  6166  xporderlem  6317  brtpos2  6337  issmo  6374  smores3  6379  tfrlem7  6403  tfrlem9  6405  tfr0dm  6408  tfri2  6452  rdgon  6472  freccllem  6488  frecfcllem  6490  frecsuclem  6492  el1o  6523  dif1o  6524  nnsucuniel  6581  elecg  6660  brecop  6712  erovlem  6714  oviec  6728  mapsncnv  6782  mptelixpg  6821  isfi  6852  enssdom  6853  map1  6904  xpcomco  6921  exmidpw  7005  exmidpweq  7006  tpfidceq  7027  fnfi  7038  fidcenumlemrks  7055  fidcenumlemrk  7056  djulclb  7157  eldju  7170  eldju2ndl  7174  eldju2ndr  7175  ctssdccl  7213  pw1nel3  7343  sucpw1nel3  7345  elni  7421  nlt1pig  7454  0nnq  7477  dfmq0qs  7542  dfplq0qs  7543  nqnq0  7554  elinp  7587  0npr  7596  ltdfpr  7619  nqprl  7664  nqpru  7665  addnqprlemfl  7672  addnqprlemfu  7673  mulnqprlemfl  7688  mulnqprlemfu  7689  cauappcvgprlemladdru  7769  suplocexprlemell  7826  addsrpr  7858  mulsrpr  7859  opelcn  7939  opelreal  7940  elreal  7941  elreal2  7943  0ncn  7944  addcnsr  7947  mulcnsr  7948  addvalex  7957  peano1nnnn  7965  peano2nnnn  7966  xrlenlt  8137  1nn  9047  peano2nn  9048  elnn0  9297  elnnne0  9309  un0addcl  9328  un0mulcl  9329  elxnn0  9360  uztrn2  9666  elnnuz  9685  elnn0uz  9686  elq  9743  elxr  9898  elfzm1b  10220  fz01or  10233  infssuzex  10376  frecfzennn  10571  inftonninf  10587  seqf  10609  ser0  10678  ser0f  10679  hashinfom  10923  iswrd  10996  clim2ser  11648  clim2ser2  11649  isermulc2  11651  iserle  11653  climserle  11656  fsum3cvg3  11707  isumclim3  11734  isumadd  11742  sumsplitdc  11743  iserabs  11786  cvgcmpub  11787  isumshft  11801  isumsplit  11802  isumlessdc  11807  cvgratz  11843  cvgratgt0  11844  clim2prod  11850  clim2divap  11851  prodf1  11853  zproddc  11890  prodsnf  11903  divides  12100  dvdsflip  12162  nninfctlemfo  12361  ialgrlemconst  12365  prm23lt5  12586  4sqlem2  12712  4sqlem12  12725  ennnfonelemjn  12773  ennnfonelem1  12778  ennnfonelemdm  12791  basmex  12891  ghmeqker  13607  isrhm  13920  rrgmex  14023  lssmex  14117  lidlmex  14237  2idlmex  14263  df2idl2  14271  2idlss  14276  psrbagf  14432  istps  14504  lmss  14718  txuni2  14728  dvply1  15237  sinq34lt0t  15303  lgsdir2lem2  15506  gausslemma2dlem1a  15535  lgsquadlem1  15554  lgsquadlem2  15555  2sqlem1  15591  bdceq  15782  bj-nntrans  15891  bj-nnelirr  15893  ss1oel2o  15932  trilpolemisumle  15981