Theorem eqeltri 1967

Description: Substitution of equal classes into membership relation.

Hypotheses

Ref	Expression
eqeltr.1	|- A = B
eqeltr.2	|- B e. C

Assertion

Ref	Expression
eqeltri	|- A e. C

Proof of Theorem eqeltri

Step	Hyp	Ref	Expression
1		eqeltr.2	. 2 |- B e. C
2		eqeltr.1	. . 3 |- A = B
3	2	eleq1i 1960	. 2 |- (A e. C <-> B e. C)
4	1, 3	mpbir 207	1 |- A e. C

Syntax hints:   = wceq 1298   e. wcel 1300

This theorem is referenced by:  eqeltrri 1968  intab 3247  inex2 3453  ord3ex 3497  zfpair 3522  opex 3527  uniopel 3556  unisn2 3799  tpex 3804  elvvuni 4055  isarep2 4499  fopabex2 4541  fvex 4689  abrexexlem2 4835  abrexex2 4847  oprex 4907  oprabex 4948  1on 5182  2on 5183  oesuc 5211  oecl 5218  oeclOLD 5219  nnecl 5285  nneclOLD 5286  1onn 5310  2onn 5311  riotaex 5564  prfi 5647  pwfi 5661  supex 5667  ordtypelem6 5689  inf0 5712  oancom 5740  rankr1 5785  hta 5858  alephon 5876  aceq5lem4 5900  aceq5lem5 5901  ac6lem 5916  kmlem10 5936  brdom7disj 5966  brdom6disj 5967  cardon 5976  cardid 5977  alephfplem1 6044  nqex 6201  srex 6331  axcnex 6419  ax1cn 6422  negex 6522  subcli 6523  xrex 6659  pnfxr 6660  pnfxrOLD 6661  mnfxr 6662  mnfxrOLD 6663  divcli 6899  redivcli 6976  nnsubi 7140  2re 7163  3re 7165  4re 7166  5re 7167  6re 7168  7re 7169  8re 7170  9re 7171  10re 7172  2nn 7183  3nn 7184  nneoi 7409  zeo 7411  om2uzuzi 7708  ser1recli 7744  ser0cl1i 7807  discrlem1 7906  sqrlem7 7929  inelr 7985  faccl 8192  facwordi 8196  faclbnd2 8198  bccl2 8223  sumex 8241  iserzshfti 8404  iserzabslem 8438  cvgcmp2lem 8440  isumshfti 8465  isumshft2i 8466  infcvglem1 8482  infcvglem2 8483  infcvglem3 8484  ivthlem5 8547  isupivthi 8552  reefcli 8579  erelem7 8587  ere 8592  efaddlem7 8606  efaddlem8 8607  efaddlem21 8620  ef1tllem 8643  absef01tlubi 8650  eirrlem2 8652  efcnlem2 8685  sin01bndlem1 8733  sin01bndlem2 8734  cos01bndlem2 8736  acdc4lem1 8756  ruclem5 8783  ruclem13 8791  ruclem15 8793  ruclem34 8812  infxpidmlem8 8828  infxpidmlem9 8829  infmap2lem2 8849  indistop 8918  fctop2 8921  lpval 9019  ismsi 9078  metxp 9111  opntop 9147  cncfmet 9183  remet 9188  rehaus 9195  lmfex 9237  fsumcnlem 9267  bcthlem12 9288  bcthlem15 9291  bcthlem30 9306  grpidvallem 9341  gxval 9381  issubg 9425  issubgi 9431  ghgrpilem4 9444  isvci 9533  isnvi 9564  imsval 9648  imsmetlem 9655  vacnlem4 9670  ipfval 9691  sspval 9721  lnoval 9752  islno 9753  nmofval 9764  nmoval 9765  bloval 9781  0ofval 9787  0oval 9788  blocni 9805  ajfval 9809  hmoval 9810  cnph 9819  isph 9822  phpar 9824  ipasslem7 9837  siilem2 9853  ajval 9863  ubthlem1 9872  ubthlem6 9877  minveclem12 9901  minveccl 9929  hlex 9947  htthlem11 9977  sincn 10018  coscn 10019  pilem3 10022  pilog 10122  fixp 10180  subsp 10244  stoiglem 10250  dvrunz 10419  normlem2 10610  normlem3 10611  normlem6 10614  shex 10710  h0elch 10760  hhsssh 10772  projlem11 10829  pjthlem1 10852  pjthlem9 10860  pjthlem10 10861  pjthlem11 10862  pjthlem12 10863  pjthlem13 10864  pjthlem14 10865  spansnji 11226  nonbooli 11231  3oalem5 11246  3oalem6 11247  3oai 11248  mayetes3i 11310  nmbdfnlb 11616  cnlnadjlem5 11641  pjbdlni 11720  golem2 11844  goeqi 11845  bnj105 12451  bnj113 12458  bnj918 12826  bnj95 13218  ghomgrpilem2 13629  ghomsn 13631  ghomgrplem 13632  cayleylem1 13641  cayleylem2 13642  cayleylem3 13643  cayleythlem 13645  divalglem5 13700  divalglem9 13704  eucalg 13755  mulgcdlem2 13757  2prm 13779  predasetex 13891  trclex 13937  altopex 14086  fixpc 14418  prodex 14656  mulveczer 14822  mulinvsca 14823  muldisc 14824  svli2 14826  hmeogrp 14892  limfillem1 14938  clindistop 14962  singempcon 14965  extopgrp 14980  topgrpsubcnlem 14981  trhom 14983  stoi 14998  lteqtpos 15024  nolimf 15031  flimfnein 15033  limnumrr 15034  cinei 15035  flimfneic 15036  flimfneicn 15037  dualalg 15131  dualded 15132  dualcat2 15133  ishomb 15137  ismona 15158  isepia 15168  cinvlem1 15176  cinvlem2 15177  isfuna 15182  issubcat 15193  infemb 15207  ordtypelem6OLD 15380  neibastop2lem1 15519  neibastop2lem4 15522  ufinffr 15578  oprabrexex2 15709  fdc 15812  piececn 15894  cncfres 15895  cnresoprab 15915  cnopropabco 15917  cnoproprabco 15919  cnoprab1 15921  cnoprab2 15922  txmet 15925  heiborlem1 15955  heiborlem3 15957  heiborlem5 15959  heiborlem7 15961  heiborlem8 15962  heiborlem20 15974  heiborlem23 15977  heiborlem25 15979  heiborlem26 15980  heiborlem29 15983  heiborlem40 15994  bfplem1 15998  bfplem2 15999  bfplem3 16000  bfplem4 16001  reheibor 16025  iccbnd 16026  grpkerinj 16042  phtpycom 16050  phtpycolem3 16053  phtpycolem4 16054  phtpcval 16058  pcocn 16076  pcorevlem 16086  pcorev 16087  isringd 16097  isdivrng1 16109  isdivrng2 16111  rnghomval 16118  isrnghom 16119  idlval 16161  isidl 16162  0idl 16173  0ring 16175  divrngidl 16176  smprngpr 16200  igenval 16209  stbex 16728  stb2v1 16745  stb2v2 16746  stb3v1 16751  stb3v2 16752  stb3v3 16753  isposNEW 16773  pgeval 16794  lubfval 16803  lubval 16804  lubprop 16805  glbfval 16808  glbval 16809  glbprop 16810  joinfval 16814  joinlem 16817  meetfval 16821  meetlem 16824  clatlem 16889  isopos 16909  cmtfval 16937  cvrfval 16987  patoms 17000  glbcon 17028  isgrpNEW 17104  grpinvfvalNEW 17125  cnaddablNEW 17139  isringNEW 17142  divrngmclNEW 17164  divrngidlemNEW 17165  divrngidNEW 17166  invrfval 17170  invrcl 17171  issrng 17176  islvec 17188  isphil 17195  plusssfval 17204  plusssval 17205  ocvfval 17206  ocvval 17207  csubspset 17208  iscsubsp 17209  lineset 17219  isline 17220  pointset 17222  psubspset 17225  ispsubsp 17226  pmapfval 17236  pmapval 17237  paddfval 17258  paddval 17259  polfval 17317  polval 17318  psubclset 17346  ispsubcl 17347  watomfval 17392  watomval 17393  pautset 17395  ispaut 17396  dilfset 17401  dilset 17402  trnfset 17404

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-cleq 1877  df-clel 1880

Copyright terms: Public domain