Theorem eqeltrri 1968

Description: Substitution of equal classes into membership relation.

Hypotheses

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

Assertion

Ref	Expression
eqeltrri	|- B e. C

Proof of Theorem eqeltrri

Step	Hyp	Ref	Expression
1		eqeltrr.1	. . 3 |- A = B
2	1	eqcomi 1888	. 2 |- B = A
3		eqeltrr.2	. 2 |- A e. C
4	2, 3	eqeltri 1967	1 |- B e. C

Syntax hints:   = wceq 1298   e. wcel 1300

This theorem is referenced by:  zfrep4 3436  pp0ex 3496  ord3ex 3497  moabex 3513  zfpair 3522  unex 3796  fvresex 4833  abrexex2 4847  abexssex 4848  abexex 4849  oprvexOLDOLD 4974  pw2en 5505  abfii2 5652  abfii4 5654  inf0 5712  scottexs 5848  kardex 5855  brdom7disj 5966  brdom6disj 5967  cardon 5976  cardid 5977  ondomon 6008  1lt2pi 6184  0cn 6481  0reALT 6604  4nn 7186  unirnioo 7571  om2uzrani 7711  sqrlem8 7930  eirrlem5 8655  ef4pi 8664  ruclem23 8801  infxpidmlem9 8829  infmap2lem2 8849  gch-kn 8856  subbas 8914  indistps 8923  distps 8924  issubg 9425  nmofval 9764  ipasslem6 9836  h2hva 10475  h2hsm 10476  h2hnm 10477  norm-ii.i 10637  shex 10710  hhshsslem2 10771  shincli 10964  chincli 11016  lnophdi 11564  bdophdi 11667  retopcon 15452  neibastop2lem1 15519  neibastop2lem4 15522  opabex3 15701  oprabrexex2 15709  bfp 16009  phtpycom 16050  phtpycolem3 16053  phtpycolem4 16054  reparphtlem2 16064  pcocn 16076  pcopt 16084  pcoass 16085  pi1bval 16088  pi1fval 16092  lineset 17219  pautset 17395

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