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

Theorem eqeltrri 2251
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 2181 . 2  |-  B  =  A
3 eqeltrr.2 . 2  |-  A  e.  C
42, 3eqeltri 2250 1  |-  B  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1353    e. wcel 2148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173
This theorem is referenced by:  3eltr3i  2258  p0ex  4185  epse  4339  unex  4438  ordtri2orexmid  4519  onsucsssucexmid  4523  ordsoexmid  4558  ordtri2or2exmid  4567  ontri2orexmidim  4568  nnregexmid  4617  abrexex  6112  opabex3  6117  abrexex2  6119  abexssex  6120  abexex  6121  oprabrexex2  6125  tfr0dm  6317  exmidonfinlem  7186  1lt2pi  7327  prarloclemarch2  7406  prarloclemlt  7480  0cn  7937  resubcli  8207  0reALT  8241  10nn  9385  numsucc  9409  nummac  9414  qreccl  9628  unirnioo  9957  fz0to4untppr  10107  fn0g  12683  sn0topon  13248  retopbas  13683  blssioo  13705  lgslem4  14064  bj-unex  14320  exmidsbthrlem  14419
  Copyright terms: Public domain W3C validator