Theorem eqeltrri 2270

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

Syntax hints:   = wceq 1364   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  3eltr3i  2277  p0ex  4222  epse  4378  unex  4477  ordtri2orexmid  4560  onsucsssucexmid  4564  ordsoexmid  4599  ordtri2or2exmid  4608  ontri2orexmidim  4609  nnregexmid  4658  abrexex  6183  opabex3  6188  abrexex2  6190  abexssex  6191  abexex  6192  oprabrexex2  6196  tfr0dm  6389  exmidonfinlem  7274  1lt2pi  7426  prarloclemarch2  7505  prarloclemlt  7579  0cn  8037  resubcli  8308  0reALT  8342  10nn  9491  numsucc  9515  nummac  9520  qreccl  9735  unirnioo  10067  fz0to4untppr  10218  4sqlem19  12605  dec2dvds  12607  modsubi  12615  gcdi  12616  prdsex  12973  fn0g  13079  fngsum  13092  sn0topon  14432  retopbas  14867  blssioo  14897  hovercncf  14990  lgslem4  15352  bj-unex  15673  exmidsbthrlem  15779