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

Theorem breq12d 3740
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Hypotheses
Ref Expression
breq1d.1
breq12d.2  C  D
Assertion
Ref Expression
breq12d  R C  R D

Proof of Theorem breq12d
StepHypRef Expression
1 breq1d.1 . 2
2 breq12d.2 . 2  C  D
3 breq12 3732 . 2  C  D  R C  R D
41, 2, 3syl2anc 391 1  R C  R D
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98   wceq 1223   class class class wbr 3727
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 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995
This theorem depends on definitions:  df-bi 110  df-3an 869  df-tru 1226  df-nf 1323  df-sb 1619  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-v 2528  df-un 2890  df-sn 3345  df-pr 3346  df-op 3348  df-br 3728
This theorem is referenced by:  breq123d  3741  3brtr3d  3756  3brtr4d  3757  pocl  4003  csbcnvg  4434  cnvpom  4775  sbcfung  4839  isoeq1  5354  isocnv  5364  isotr  5369  caovordig  5577  caovordg  5579  caovord2d  5581  caovord  5583  ofrfval  5631  ofrval  5633  ofrfval2  5638  caofref  5643  nqtri3or  6241  ltsonq  6243  ltanqg  6245  ltmnqg  6246  lt2addnq  6249  prarloclemarch  6261  ltrnqg  6263  prarloclemlt  6333  addlocprlemgt  6375  mullocprlem  6400  addextpr  6442  recexprlemss1l  6456  recexprlemss1u  6457  recexpr  6459  lttrsr  6500  ltposr  6501  ltsosr  6502  ltasrg  6508  aptisr  6515  mulextsr1lem  6516  mulextsr1  6517  axpre-ltirr  6571  axpre-ltadd  6575  axpre-mulgt0  6576  axpre-mulext  6577  ltadd2  7015  ltadd1  7022  leadd2  7024  reapval  7163  reapmul1  7182  remulext2  7187  apreim  7190  apirr  7192  apsym  7193  apcotr  7194  apadd1  7195  apadd2  7196  apneg  7198  mulext1  7199  mulext2  7200  apti  7209  apmul1  7349  ltmul2  7405  lemul2  7406  ltdiv1  7417  ltdiv2  7436  ledivdiv  7439  lediv2  7440  qapne  8056
  Copyright terms: Public domain W3C validator