Theorem eqeltrri 2244

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

Syntax hints:   = wceq 1348   e. wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  3eltr3i  2251  p0ex  4174  epse  4327  unex  4426  ordtri2orexmid  4507  onsucsssucexmid  4511  ordsoexmid  4546  ordtri2or2exmid  4555  ontri2orexmidim  4556  nnregexmid  4605  abrexex  6096  opabex3  6101  abrexex2  6103  abexssex  6104  abexex  6105  oprabrexex2  6109  tfr0dm  6301  exmidonfinlem  7170  1lt2pi  7302  prarloclemarch2  7381  prarloclemlt  7455  0cn  7912  resubcli  8182  0reALT  8216  10nn  9358  numsucc  9382  nummac  9387  qreccl  9601  unirnioo  9930  fz0to4untppr  10080  fn0g  12629  sn0topon  12882  retopbas  13317  blssioo  13339  lgslem4  13698  bj-unex  13954  exmidsbthrlem  14054