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

Theorem eqeltrri 2215
 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 2145 . 2
3 eqeltrr.2 . 2
42, 3eqeltri 2214 1
 Colors of variables: wff set class Syntax hints:   wceq 1332   wcel 2112 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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1487  ax-17 1503  ax-ial 1511  ax-ext 2123 This theorem depends on definitions:  df-bi 116  df-cleq 2134  df-clel 2137 This theorem is referenced by:  3eltr3i  2222  p0ex  4122  epse  4275  unex  4373  ordtri2orexmid  4449  onsucsssucexmid  4453  ordsoexmid  4488  ordtri2or2exmid  4497  nnregexmid  4546  abrexex  6027  opabex3  6032  abrexex2  6034  abexssex  6035  abexex  6036  oprabrexex2  6040  tfr0dm  6231  exmidonfinlem  7078  1lt2pi  7201  prarloclemarch2  7280  prarloclemlt  7354  0cn  7811  resubcli  8078  0reALT  8112  10nn  9250  numsucc  9274  nummac  9279  qreccl  9490  unirnioo  9815  sn0topon  12332  retopbas  12767  blssioo  12789  bj-unex  13333  exmidsbthrlem  13436
 Copyright terms: Public domain W3C validator