Theorem eleq2i 2166

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 2163	. 2 |- ( A = B -> ( C e. A <-> C e. B ) )
3	1, 2	ax-mp 7	1 |- ( C e. A <-> C e. B )

Syntax hints:   <-> wb 104   = wceq 1299   e. wcel 1448

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093  df-clel 2096

This theorem is referenced by:  eleq12i  2167  eleqtri  2174  eleq2s  2194  hbxfreq  2206  abeq2i  2210  abeq1i  2211  nfceqi  2236  raleqbii  2406  rexeqbii  2407  rabeq2i  2638  elab2g  2784  elrabf  2791  elrab3t  2792  elrab2  2796  cbvsbc  2889  elin2  3211  dfnul2  3312  noel  3314  rabn0m  3337  rabeq0  3339  eltpg  3516  tpid3g  3585  oprcl  3676  elunirab  3696  elintrab  3730  exss  4087  elop  4091  opm  4094  brabsb  4121  brabga  4124  pofun  4172  elsuci  4263  elsucg  4264  elsuc2g  4265  ordsucim  4354  peano2  4447  elxp  4494  brab2a  4530  brab2ga  4552  elco  4643  elcnv  4654  dmmrnm  4696  elrnmptg  4729  opelres  4760  rninxp  4918  funco  5099  elfv  5351  nfvres  5386  fvopab3g  5426  fvmptssdm  5437  fmptco  5518  funfvima  5581  fliftel  5626  acexmidlema  5697  acexmidlemb  5698  acexmidlem2  5703  eloprabga  5790  elrnmpo  5816  ovid  5819  offval  5921  xporderlem  6058  brtpos2  6078  issmo  6115  smores3  6120  tfrlem7  6144  tfrlem9  6146  tfr0dm  6149  tfri2  6193  rdgon  6213  freccllem  6229  frecfcllem  6231  frecsuclem  6233  el1o  6264  dif1o  6265  nnsucuniel  6321  elecg  6397  brecop  6449  erovlem  6451  oviec  6465  mapsncnv  6519  mptelixpg  6558  isfi  6585  enssdom  6586  map1  6636  xpcomco  6649  exmidpw  6731  fnfi  6753  fidcenumlemrks  6769  fidcenumlemrk  6770  djulclb  6855  eldju  6868  eldju2ndl  6872  eldju2ndr  6873  ctssdclemr  6911  elni  7017  nlt1pig  7050  0nnq  7073  dfmq0qs  7138  dfplq0qs  7139  nqnq0  7150  elinp  7183  0npr  7192  ltdfpr  7215  nqprl  7260  nqpru  7261  addnqprlemfl  7268  addnqprlemfu  7269  mulnqprlemfl  7284  mulnqprlemfu  7285  cauappcvgprlemladdru  7365  addsrpr  7441  mulsrpr  7442  opelcn  7514  opelreal  7515  elreal  7516  elreal2  7518  0ncn  7519  addcnsr  7521  mulcnsr  7522  addvalex  7531  peano1nnnn  7539  peano2nnnn  7540  xrlenlt  7701  1nn  8589  peano2nn  8590  elnn0  8831  elnnne0  8843  un0addcl  8862  un0mulcl  8863  elxnn0  8894  uztrn2  9193  elnnuz  9212  elnn0uz  9213  elq  9264  elxr  9404  elfzm1b  9719  fz01or  9732  frecfzennn  10040  inftonninf  10055  seqf  10075  ser0  10128  ser0f  10129  hashinfom  10365  clim2ser  10945  clim2ser2  10946  isermulc2  10948  iserle  10950  climserle  10953  fsum3cvg3  11004  isumclim3  11031  isumadd  11039  sumsplitdc  11040  iserabs  11083  cvgcmpub  11084  isumshft  11098  isumsplit  11099  isumlessdc  11104  cvgratz  11140  cvgratgt0  11141  divides  11290  dvdsflip  11344  infssuzex  11437  ialgrlemconst  11517  ennnfonelemjn  11707  ennnfonelem1  11712  ennnfonelemdm  11725  istps  11981  lmss  12196  txuni2  12206  bdceq  12621  bj-nntrans  12734  bj-nnelirr  12736  ss1oel2o  12774  trilpolemisumle  12815