Theorem eqeltr 1547

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 1540	. 2 |- (A e. C <-> B e. C)
4	1, 3	mpbir 190	1 |- A e. C

Syntax hints:   = wceq 958   e. wcel 960

This theorem is referenced by:  eqeltrr 1548  intab 2564  inex2 2722  zfpair 2783  opex 2788  uniopel 2815  unisn2 2881  tpex 2884  elvvuni 3235  isarep2 3584  fopabex2 3618  fvex 3738  abrexexlem2 3865  abrexex2 3877  oprex 3989  oprabex 4025  1on 4144  oesuc 4172  oecl 4178  nnecl 4237  1onn 4259  2onn 4260  prfi 4568  pwfi 4579  supex 4586  inf0 4615  oancom 4642  rankr1 4684  hta 4738  aceq5lem4 4748  aceq5lem5 4749  ac6lem 4764  kmlem10 4784  brdom7disj 4814  brdom6disj 4815  cardon 4837  cardid 4838  alephon 4876  alephfplem1 4907  nqex 5061  srex 5191  axcnex 5279  ax1cn 5281  negex 5377  subcl 5378  xrex 5504  pnfxr 5505  mnfxr 5506  pnfnemnf 5548  divcl 5722  redivcl 5800  nnsub 5958  2re 5981  3re 5983  4re 5984  5re 5985  6re 5986  7re 5987  8re 5988  9re 5989  10re 5990  2nn 6001  3nn 6002  nneo 6199  zeot 6201  om2uzuz 6298  ser1recl 6332  ser0cl1 6565  discrlem1 6657  sqrlem7 6680  inelr 6736  facclt 6940  facwordit 6944  faclbnd2 6946  bccl2t 6971  sumex 6981  iserzshft 7144  iserzabslem 7178  cvgcmp2lem 7180  isumshft 7204  isumshft2 7205  infcvglem1 7221  infcvglem2 7222  infcvglem3 7223  ivthlem5 7285  isupivth 7290  reefcl 7317  erelem7 7325  ere 7330  efaddlem7 7344  efaddlem8 7345  efaddlem21 7358  ef1tllem 7381  absef01tlub 7388  eirrlem2 7390  efcnlem2 7420  sin01bndlem1 7468  sin01bndlem2 7469  cos01bndlem2 7471  ruclem5 7515  ruclem13 7523  ruclem15 7525  ruclem34 7544  infxpidmlem8 7560  infxpidmlem9 7561  infmap2lem2 7582  indistop 7645  fctop2OLD 7648  lpval 7740  ismsi 7798  metxp 7831  opntop 7867  cncfmet 7902  remet 7907  rehaus 7914  lmfex 7956  fsumcnlem 7986  bcthlem12 8007  bcthlem15 8010  bcthlem30 8025  issubg 8112  issubgi 8118  ghgrpilem4 8132  isvci 8197  isnvi 8228  imsval 8312  imsmetlem 8319  ipfval 8348  sspval 8378  lnoval 8409  islno 8410  nmofval 8421  nmoval 8422  bloval 8437  0ofval 8443  0oval 8444  blocni 8461  ajfval 8465  hmoval 8466  cnph 8474  isph 8477  phpar 8479  ipasslem7 8492  siilem2 8508  ubthlem1 8525  ubthlem6 8530  minveclem12 8552  minveccl 8580  hlex 8596  htthlem11 8626  sincn 8664  coscn 8665  pilem3 8668  pilog 8763  normlem2 8972  normlem3 8973  normlem6 8976  shex 9072  h0elch 9122  hhsssh 9134  projlem11 9191  pjthlem1 9214  pjthlem9 9222  pjthlem10 9223  pjthlem11 9224  pjthlem12 9225  pjthlem13 9226  pjthlem14 9227  spansnj 9586  nonbool 9591  3oalem5 9606  3oalem6 9607  3oa 9608  nmbdfnlbt 9974  cnlnadjlem5 9999  pjbdln 10071  golem2 10194  goeq 10195  ghomgrpilem2 10381  ghomsn 10383  ghomgrplem 10384  cayleylem1 10404  cayleylem2 10405  cayleylem3 10406  cayleythlem 10408  hmeogrp 10524  subsp 10540  limfillem1OLD 10578  stoi 10610  ishomb 10687  ismona 10708  isepia 10718  isfuna 10725

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-cleq 1472  df-clel 1475

Copyright terms: Public domain