Theorem eleqtrr 1539

Description: Substitution of equal classes into membership relation.

Hypotheses

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

Assertion

Ref	Expression
eleqtrr	|- A e. C

Proof of Theorem eleqtrr

Step	Hyp	Ref	Expression
1		eleqtrr.1	. 2 |- A e. B
2		eleqtrr.2	. . 3 |- C = B
3	2	eqcomi 1471	. 2 |- B = C
4	1, 3	eleqtr 1538	1 |- A e. C

Syntax hints:   = wceq 953   e. wcel 955

This theorem is referenced by:  opi1 2774  opi2 2775  oneo 4196  0elixp 4344  pw2en 4426  oancom 4605  tz9.13 4635  rankid 4644  rankpw 4656  1lt2pi 5004  pnfxr 5465  mnfxr 5466  1nn 5882  infcvgaux1 7154  abscncfALT 8278  blocni 8396  sincnlem 8585  pilog 8690  projlem8 9109  nonbool 9513  nmopadjle 9936  hmopidmch 9990  1ded 10515

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465

Copyright terms: Public domain