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

Theorem breqtrri 4029
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
breqtrr.1 𝐴𝑅𝐵
breqtrr.2 𝐶 = 𝐵
Assertion
Ref Expression
breqtrri 𝐴𝑅𝐶

Proof of Theorem breqtrri
StepHypRef Expression
1 breqtrr.1 . 2 𝐴𝑅𝐵
2 breqtrr.2 . . 3 𝐶 = 𝐵
32eqcomi 2181 . 2 𝐵 = 𝐶
41, 3breqtri 4027 1 𝐴𝑅𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1353   class class class wbr 4002
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-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4003
This theorem is referenced by:  3brtr4i  4032  ensn1  6793  pw1dom2  7223  0lt1sr  7761  0le2  9005  2pos  9006  3pos  9009  4pos  9012  5pos  9015  6pos  9016  7pos  9017  8pos  9018  9pos  9019  1lt2  9084  2lt3  9085  3lt4  9087  4lt5  9090  5lt6  9094  6lt7  9099  7lt8  9105  8lt9  9112  nn0le2xi  9222  numltc  9405  declti  9417  sqge0i  10601  faclbnd2  10715  ege2le3  11672  cos2bnd  11761  3dvdsdec  11862  n2dvdsm1  11910  n2dvds3  11912  pockthi  12348  dveflem  14058  tangtx  14130  lgsdir2lem2  14301  ex-fl  14337
  Copyright terms: Public domain W3C validator