ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqeltrri Structured version   GIF version

Theorem eqeltrri 2093
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqeltrr.1 A = B
eqeltrr.2 A 𝐶
Assertion
Ref Expression
eqeltrri B 𝐶

Proof of Theorem eqeltrri
StepHypRef Expression
1 eqeltrr.1 . . 3 A = B
21eqcomi 2026 . 2 B = A
3 eqeltrr.2 . 2 A 𝐶
42, 3eqeltri 2092 1 B 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1228   wcel 1374
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015  df-clel 2018
This theorem is referenced by:  3eltr3i  2100  p0ex  3913  epse  4047  unex  4126  ordtri2orexmid  4195  onsucsssucexmid  4196  ordsoexmid  4224  nnregexmid  4269  abrexex  5667  opabex3  5672  abrexex2  5674  abexssex  5675  abexex  5676  oprabrexex2  5680  1lt2pi  6200  prarloclemarch2  6276  prarloclemlt  6347  0cn  6621  resubcli  6866  0reALT  6900  bj-unex  7289
  Copyright terms: Public domain W3C validator