Theorem eleq2i 2299

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 2296	. 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 1398   e. wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  eleq12i  2300  eleqtri  2307  eleq2s  2327  hbxfreq  2339  abeq2i  2343  abeq1i  2344  nfceqi  2380  raleqbii  2554  rexeqbii  2555  rabeq2i  2809  elab2g  2963  elrabf  2970  elrab3t  2971  elrab2  2975  cbvsbcw  3069  cbvsbc  3070  csbcow  3148  elin2  3406  dfnul2  3509  noel  3511  rabn0m  3535  rabeq0  3537  eltpg  3733  tpid3g  3806  oprcl  3906  elunirab  3926  elintrab  3960  exss  4342  elop  4346  opm  4349  brabsb  4378  brabga  4381  pofun  4432  elsuci  4523  elsucg  4524  elsuc2g  4525  ordsucim  4621  peano2  4716  elxp  4765  brab2a  4802  brab2ga  4824  elco  4920  elcnv  4931  dmmrnm  4975  elrnmptg  5008  opelres  5042  rninxp  5205  eliota  5339  funco  5391  elfv  5667  nfvres  5705  fvopab3g  5749  fvmptssdm  5761  fmptco  5842  funfvima  5917  fliftel  5965  acexmidlema  6040  acexmidlemb  6041  acexmidlem2  6046  eloprabga  6139  elrnmpo  6166  ovid  6169  offval  6273  xporderlem  6426  brtpos2  6481  issmo  6518  smores3  6523  tfrlem7  6547  tfrlem9  6549  tfr0dm  6552  tfri2  6596  rdgon  6616  freccllem  6632  frecfcllem  6634  frecsuclem  6636  el1o  6669  dif1o  6670  nnsucuniel  6727  elecg  6806  brecop  6858  erovlem  6860  oviec  6874  mapsncnv  6929  mptelixpg  6968  isfi  6999  enssdom  7000  map1  7053  xpcomco  7076  exmidpw  7167  exmidpweq  7168  tpfidceq  7189  fnfi  7202  fidcenumlemrks  7222  fidcenumlemrk  7223  djulclb  7345  eldju  7358  eldju2ndl  7362  eldju2ndr  7363  ctssdccl  7401  pw1nel3  7540  sucpw1nel3  7542  elni  7619  nlt1pig  7652  0nnq  7675  dfmq0qs  7740  dfplq0qs  7741  nqnq0  7752  elinp  7785  0npr  7794  ltdfpr  7817  nqprl  7862  nqpru  7863  addnqprlemfl  7870  addnqprlemfu  7871  mulnqprlemfl  7886  mulnqprlemfu  7887  cauappcvgprlemladdru  7967  suplocexprlemell  8024  addsrpr  8056  mulsrpr  8057  opelcn  8137  opelreal  8138  elreal  8139  elreal2  8141  0ncn  8142  addcnsr  8145  mulcnsr  8146  addvalex  8155  peano1nnnn  8163  peano2nnnn  8164  xrlenlt  8334  1nn  9244  peano2nn  9245  elnn0  9494  elnnne0  9506  un0addcl  9525  un0mulcl  9526  elxnn0  9561  uztrn2  9868  elnnuz  9887  elnn0uz  9888  elq  9950  elxr  10105  elfzm1b  10428  fz01or  10441  infssuzex  10589  frecfzennn  10784  inftonninf  10800  seqf  10822  ser0  10891  ser0f  10892  hashinfom  11136  iswrd  11219  pfxccatpfx1  11421  clim2ser  12015  clim2ser2  12016  isermulc2  12018  iserle  12020  climserle  12023  fsum3cvg3  12075  isumclim3  12102  isumadd  12110  sumsplitdc  12111  iserabs  12154  cvgcmpub  12155  isumshft  12169  isumsplit  12170  isumlessdc  12175  cvgratz  12211  cvgratgt0  12212  clim2prod  12218  clim2divap  12219  prodf1  12221  zproddc  12258  prodsnf  12271  divides  12468  dvdsflip  12530  nninfctlemfo  12729  ialgrlemconst  12733  prm23lt5  12954  4sqlem2  13080  4sqlem12  13093  ennnfonelemjn  13142  ennnfonelem1  13147  ennnfonelemdm  13160  basmex  13261  ghmeqker  13977  isrhm  14292  rrgmex  14395  lssmex  14490  lidlmex  14610  2idlmex  14636  df2idl2  14644  2idlss  14649  psrbagf  14805  istps  14884  lmss  15098  txuni2  15108  dvply1  15617  sinq34lt0t  15683  lgsdir2lem2  15889  gausslemma2dlem1a  15918  lgsquadlem1  15937  lgsquadlem2  15938  2sqlem1  15974  isuhgrm  16053  isushgrm  16054  isupgren  16077  isumgren  16087  umgredg  16127  umgrpredgv  16129  umgredgne  16132  umgredgnlp  16134  isuspgren  16139  isusgren  16140  ausgrusgrien  16153  usgredgppren  16179  edgssv2en  16181  uspgredg2vlem  16202  uspgredg2v  16203  ushgredgedg  16208  ushgredgedgloop  16210  griedg0ssusgr  16233  uhgrissubgr  16243  subumgredg2en  16253  uhgrspansubgrlem  16258  vtxedgfi  16271  vtxlpfi  16272  vtxdg0v  16276  wlk1walkdom  16341  clwwlkccatlem  16382  clwwlknnn  16394  clwwlknon2x  16417  bdceq  16599  bj-nntrans  16708  bj-nnelirr  16710  ss1oel2o  16748  trilpolemisumle  16809