Theorem eqeltr 1541

Description: Substitution of equal classes into membership relation.

Hypotheses

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

Assertion

Ref	Expression
eqeltr	|- A e. C

Proof of Theorem eqeltr

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

Syntax hints:   = wceq 954   e. wcel 956

This theorem is referenced by:  eqeltrr 1542  intab 2555  inex2 2712  zfpair 2772  opex 2777  uniopel 2804  unisn2 2870  tpex 2873  elvvuni 3224  isarep2 3570  fopabex2 3604  fvex 3723  abrexexlem2 3850  abrexex2 3862  oprex 3974  oprabex 4010  1on 4128  oesuc 4156  oecl 4162  nnecl 4221  1onn 4243  2onn 4244  supex 4557  inf0 4586  oancom 4613  rankr1 4654  hta 4708  aceq5lem4 4718  aceq5lem5 4719  ac6lem 4734  kmlem10 4754  brdom7disj 4784  brdom6disj 4785  cardon 4807  cardid 4808  alephon 4845  alephfplem1 4876  nqex 5029  srex 5159  axcnex 5247  ax1cn 5249  negex 5345  subcl 5346  xrex 5472  pnfxr 5473  mnfxr 5474  pnfnemnf 5517  divcl 5687  redivcl 5762  nnsub 5911  2re 5934  3re 5936  4re 5937  5re 5938  6re 5939  7re 5940  8re 5941  9re 5942  10re 5943  2nn 5954  3nn 5955  nneo 6152  zeot 6154  om2uzuz 6242  ser1recl 6276  ser0cl1 6504  discrlem1 6594  sqrlem7 6617  inelr 6673  facclt 6885  facwordit 6889  faclbnd2 6891  bccl2t 6917  sumex 6927  iserzshft 7088  iserzabslem 7122  cvgcmp2lem 7124  isumshft 7147  isumshft2 7148  infcvglem1 7164  infcvglem2 7165  infcvglem3 7166  ivthlem5 7228  isupivth 7233  ivthlem5OLD 7237  reefcl 7267  erelem7 7275  ere 7280  efaddlem7 7294  efaddlem8 7295  efaddlem21 7308  ef1tllem 7331  absef01tlub 7337  eirrlem2 7339  efcnlem2 7368  sin01bndlem1 7417  sin01bndlem2 7418  cos01bndlem2 7420  ruclem5 7465  ruclem13 7473  ruclem15 7475  ruclem34 7494  infxpidmlem8 7510  infxpidmlem9 7511  infmap2lem2 7530  indistop 7598  fctop2 7601  lpval 7693  ismsi 7751  metxp 7786  opntop 7822  cncfmet 7857  remet 7862  rehaus 7869  lmfex 7910  fsumcnlem 7939  bcthlem12 7960  bcthlem15 7963  bcthlem30 7978  issubg 8068  issubgi 8074  ghgrpilem4 8088  isvci 8153  isnvi 8184  imsval 8267  imsmetlem 8274  ipfval 8299  sspval 8329  lnoval 8360  islno 8361  nmofval 8370  nmoval 8371  bloval 8386  0ofval 8392  0oval 8393  blocni 8409  ajfval 8413  hmoval 8414  cnph 8422  isph 8425  phpar 8427  ipasslem7 8440  siilem2 8456  ubthlem1 8473  ubthlem6 8478  minveclem12 8500  minveccl 8528  hlex 8543  htthlem11 8573  sincn 8607  coscn 8608  pilem3 8611  circgrpOLD 8677  pilog 8707  normlem2 8916  normlem3 8917  normlem6 8920  shex 9016  h0elch 9066  hhsssh 9078  projlem11 9135  pjthlem1 9157  pjthlem9 9165  pjthlem10 9166  pjthlem11 9167  pjthlem12 9168  pjthlem13 9169  pjthlem14 9170  spansnj 9531  nonbool 9536  3oalem5 9551  3oalem6 9552  3oa 9553  nmbdfnlbt 9917  cnlnadjlem5 9942  pjbdln 10014  golem2 10137  goeq 10138  ghomgrpilem2 10320  ghomsn 10322  ghomgrplem 10323  cayleylem1 10343  cayleylem2 10344  cayleylem3 10345  cayleythlem 10347  hmeogrp 10461  subsp 10465  dtopcl 10495  stoi 10519  ishomb 10596  ismona 10615  isfuna 10628

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-cleq 1467  df-clel 1470

Copyright terms: Public domain