Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqnbrtrd Structured version   Visualization version   GIF version

Theorem eqnbrtrd 5052
 Description: Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
Hypotheses
Ref Expression
eqnbrtrd.1 (𝜑𝐴 = 𝐵)
eqnbrtrd.2 (𝜑 → ¬ 𝐵𝑅𝐶)
Assertion
Ref Expression
eqnbrtrd (𝜑 → ¬ 𝐴𝑅𝐶)

Proof of Theorem eqnbrtrd
StepHypRef Expression
1 eqnbrtrd.2 . 2 (𝜑 → ¬ 𝐵𝑅𝐶)
2 eqnbrtrd.1 . . 3 (𝜑𝐴 = 𝐵)
32breq1d 5044 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
41, 3mtbird 328 1 (𝜑 → ¬ 𝐴𝑅𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   class class class wbr 5034 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3444  df-un 3888  df-sn 4529  df-pr 4531  df-op 4535  df-br 5035 This theorem is referenced by:  supgtoreq  8936  rlimno1  15022  pczndvds  16211  pcadd  16235  recld2  23460  itg2cnlem2  24407  dgrub  24875  gausslemma2dlem1a  25993  mirbtwnhl  26518  nosupprefixmo  33390  nosupbnd1lem1  33398  nosupbnd2lem1  33405  noinfbnd1lem1  33413  noinfbnd2  33421  sqrtcval  40512
 Copyright terms: Public domain W3C validator