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

Theorem breqtrri 3862
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
breqtrr.1  |-  A R B
breqtrr.2  |-  C  =  B
Assertion
Ref Expression
breqtrri  |-  A R C

Proof of Theorem breqtrri
StepHypRef Expression
1 breqtrr.1 . 2  |-  A R B
2 breqtrr.2 . . 3  |-  C  =  B
32eqcomi 2092 . 2  |-  B  =  C
41, 3breqtri 3860 1  |-  A R C
Colors of variables: wff set class
Syntax hints:    = wceq 1289   class class class wbr 3837
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-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-un 3001  df-sn 3447  df-pr 3448  df-op 3450  df-br 3838
This theorem is referenced by:  3brtr4i  3865  ensn1  6493  0lt1sr  7290  0le2  8483  2pos  8484  3pos  8487  4pos  8490  5pos  8493  6pos  8494  7pos  8495  8pos  8496  9pos  8497  1lt2  8555  2lt3  8556  3lt4  8558  4lt5  8561  5lt6  8565  6lt7  8570  7lt8  8576  8lt9  8583  nn0le2xi  8693  numltc  8871  declti  8883  sqge0i  10006  faclbnd2  10115  3dvdsdec  10958  n2dvdsm1  11006  n2dvds3  11008  ex-fl  11309  pw1dom2  11546
  Copyright terms: Public domain W3C validator