Theorem eleqtrr 1547

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

Syntax hints:   = wceq 956   e. wcel 958

This theorem is referenced by:  opi1 2784  opi2 2785  oneo 4212  0elixp 4360  pw2en 4446  oancom 4633  tz9.13 4663  rankid 4672  rankpw 4684  1lt2pi 5032  pnfxr 5493  mnfxr 5494  1nn 5934  infcvgaux1 7219  abscncfALT 8344  blocni 8465  sincnlem 8666  pilog 8768  projlem8 9193  nonbool 9596  nmopadjle 10021  hmopidmch 10079  1ded 10671

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain