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

Theorem breq1d 3744
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1d.1 (φA = B)
Assertion
Ref Expression
breq1d (φ → (A𝑅𝐶B𝑅𝐶))

Proof of Theorem breq1d
StepHypRef Expression
1 breq1d.1 . 2 (φA = B)
2 breq1 3737 . 2 (A = B → (A𝑅𝐶B𝑅𝐶))
31, 2syl 14 1 (φ → (A𝑅𝐶B𝑅𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1226   class class class wbr 3734
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-v 2533  df-un 2895  df-sn 3352  df-pr 3353  df-op 3355  df-br 3735
This theorem is referenced by:  eqbrtrd  3754  syl6eqbr  3771  sbcbr2g  3786  pofun  4019  fmptco  5251  isorel  5369  isocnv  5372  isotr  5377  caovordig  5585  caovordg  5587  caovord  5591  xporderlem  5770  reldmtpos  5786  brtposg  5787  tpostpos  5797  tposoprab  5813  th3qlem2  6116  ltsonq  6251  ltanqg  6253  ltmnqg  6254  archnqq  6268  prloc  6339  addnqprulem  6377  appdivnq  6401  mulnqpru  6407  mullocprlem  6408  1idpru  6424  ltsosr  6505  ltasrg  6511  addgt0sr  6515  axpre-ltadd  6573  ltsubadd  7012  lesubadd  7014  ltaddsub2  7017  leaddsub2  7019  ltaddpos  7032  lesub2  7037  ltsub2  7039  ltnegcon2  7044  lenegcon2  7047  addge01  7052  subge0  7054  suble0  7055
  Copyright terms: Public domain W3C validator