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

Theorem eqeltrri 2153
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
StepHypRef Expression
1 eqeltrr.1 . . 3  |-  A  =  B
21eqcomi 2086 . 2  |-  B  =  A
3 eqeltrr.2 . 2  |-  A  e.  C
42, 3eqeltri 2152 1  |-  B  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1285    e. wcel 1434
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078
This theorem is referenced by:  3eltr3i  2160  p0ex  3967  epse  4105  unex  4202  ordtri2orexmid  4274  onsucsssucexmid  4278  ordsoexmid  4313  ordtri2or2exmid  4322  nnregexmid  4368  abrexex  5775  opabex3  5780  abrexex2  5782  abexssex  5783  abexex  5784  oprabrexex2  5788  tfr0dm  5971  1lt2pi  6592  prarloclemarch2  6671  prarloclemlt  6745  0cn  7173  resubcli  7438  0reALT  7472  10nn  8573  numsucc  8597  nummac  8602  qreccl  8808  unirnioo  9072  bj-unex  10868
  Copyright terms: Public domain W3C validator