Theorem eleqtrr 1544

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 1476	. 2 |- B = C
4	1, 3	eleqtr 1543	1 |- A e. C

Syntax hints:   = wceq 954   e. wcel 956

This theorem is referenced by:  opi1 2779  opi2 2780  oneo 4202  0elixp 4350  pw2en 4432  oancom 4613  tz9.13 4643  rankid 4652  rankpw 4664  1lt2pi 5012  pnfxr 5473  mnfxr 5474  1nn 5890  infcvgaux1 7162  abscncfALT 8291  blocni 8409  sincnlem 8604  pilog 8707  projlem8 9132  nonbool 9536  nmopadjle 9959  hmopidmch 10017  1ded 10551

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