Theorem eqeltrri 2251

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)

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 2181	. 2 |- B = A
3		eqeltrr.2	. 2 |- A e. C
4	2, 3	eqeltri 2250	1 |- B e. C

Syntax hints:   = wceq 1353   e. wcel 2148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  3eltr3i  2258  p0ex  4190  epse  4344  unex  4443  ordtri2orexmid  4524  onsucsssucexmid  4528  ordsoexmid  4563  ordtri2or2exmid  4572  ontri2orexmidim  4573  nnregexmid  4622  abrexex  6120  opabex3  6125  abrexex2  6127  abexssex  6128  abexex  6129  oprabrexex2  6133  tfr0dm  6325  exmidonfinlem  7194  1lt2pi  7341  prarloclemarch2  7420  prarloclemlt  7494  0cn  7951  resubcli  8222  0reALT  8256  10nn  9401  numsucc  9425  nummac  9430  qreccl  9644  unirnioo  9975  fz0to4untppr  10126  prdsex  12723  fn0g  12799  sn0topon  13627  retopbas  14062  blssioo  14084  lgslem4  14443  bj-unex  14710  exmidsbthrlem  14809