Theorem eqeltrri 2312

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

This proof depends on syntax axioms:   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  3eltr3i  2319  p0ex  4327  epse  4489  unex  4589  ordtri2orexmid  4672  onsucsssucexmid  4676  ordsoexmid  4711  ordtri2or2exmid  4720  ontri2orexmidim  4721  nnregexmid  4770  abrexex  6350  opabex3  6355  abrexex2  6357  abexssex  6358  abexex  6359  oprabrexex2  6367  tfr0dm  6598  exmidonfinlem  7551  1lt2pi  7713  prarloclemarch2  7792  prarloclemlt  7866  0cn  8324  resubcli  8596  0reALT  8630  10nn  9806  numsucc  9831  nummac  9836  qreccl  10057  unirnioo  10391  fz0to4untppr  10547  cats1fvn  11557  4sqlem19  13216  dec2dvds  13218  mod2xnegi  13226  modsubi  13227  gcdi  13228  ballotfilemth  13338  fn0g  13753  fngzsum  13766  prdsex  14278  sn0topon  15331  retopbas  15766  blssioo  15796  hovercncf  15889  log2ublem2  16239  log2ublog2  16241  ppi1i  16289  cht2  16293  cht3  16294  bpos1lem  16326  lgslem4  16344  konigsberglem1  16951  bj-unex  17167  exmidsbthrlem  17290