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

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

Proof of Theorem eqeltrri
StepHypRef Expression
1 eqeltrr.1 . . 3 𝐴 = 𝐵
21eqcomi 2093 . 2 𝐵 = 𝐴
3 eqeltrr.2 . 2 𝐴𝐶
42, 3eqeltri 2161 1 𝐵𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1290  wcel 1439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473  ax-ext 2071
This theorem depends on definitions:  df-bi 116  df-cleq 2082  df-clel 2085
This theorem is referenced by:  3eltr3i  2169  p0ex  4029  epse  4178  unex  4276  ordtri2orexmid  4352  onsucsssucexmid  4356  ordsoexmid  4391  ordtri2or2exmid  4400  nnregexmid  4447  abrexex  5902  opabex3  5907  abrexex2  5909  abexssex  5910  abexex  5911  oprabrexex2  5915  tfr0dm  6101  1lt2pi  6953  prarloclemarch2  7032  prarloclemlt  7106  0cn  7534  resubcli  7799  0reALT  7833  10nn  8946  numsucc  8970  nummac  8975  qreccl  9181  unirnioo  9445  sn0topon  11842  bj-unex  12076  exmidsbthrlem  12178
  Copyright terms: Public domain W3C validator