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

Theorem breq12d 3942
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  |-  ( ph  ->  A  =  B )
breq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
breq12d  |-  ( ph  ->  ( A R C  <-> 
B R D ) )

Proof of Theorem breq12d
StepHypRef Expression
1 breq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 breq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 breq12 3934 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2anc 408 1  |-  ( ph  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1331   class class class wbr 3929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930
This theorem is referenced by:  breq123d  3943  3brtr3d  3959  3brtr4d  3960  pocl  4225  csbcnvg  4723  cnvpom  5081  sbcfung  5147  isoeq1  5702  isocnv  5712  isotr  5717  caovordig  5936  caovordg  5938  caovord2d  5940  caovord  5942  ofrfval  5990  ofrval  5992  ofrfval2  5998  caofref  6003  fundmeng  6701  xpsneng  6716  xpcomeng  6722  xpdom2g  6726  phplem3g  6750  php5  6752  php5dom  6757  nqtri3or  7218  ltsonq  7220  ltanqg  7222  ltmnqg  7223  lt2addnq  7226  lt2mulnq  7227  prarloclemarch  7240  ltrnqg  7242  ltnnnq  7245  prarloclemlt  7315  addlocprlemgt  7356  mullocprlem  7392  addextpr  7443  recexprlemss1l  7457  recexprlemss1u  7458  recexpr  7460  caucvgprlemcanl  7466  cauappcvgprlemm  7467  cauappcvgprlemdisj  7473  cauappcvgprlemloc  7474  cauappcvgprlemladdru  7478  cauappcvgprlemladdrl  7479  cauappcvgprlem1  7481  cauappcvgprlemlim  7483  cauappcvgpr  7484  caucvgprlemnkj  7488  caucvgprlemnbj  7489  caucvgprlemdisj  7496  caucvgprlemloc  7497  caucvgprlemcl  7498  caucvgprlemladdrl  7500  caucvgprlem1  7501  caucvgpr  7504  caucvgprprlemell  7507  caucvgprprlemcbv  7509  caucvgprprlemval  7510  caucvgprprlemnkeqj  7512  caucvgprprlemopl  7519  caucvgprprlemlol  7520  caucvgprprlemloc  7525  caucvgprprlemclphr  7527  caucvgprprlemexb  7529  caucvgprprlem1  7531  lttrsr  7584  ltposr  7585  ltsosr  7586  ltasrg  7592  aptisr  7601  mulextsr1lem  7602  mulextsr1  7603  caucvgsrlemcau  7615  caucvgsrlemgt1  7617  caucvgsrlemoffcau  7620  caucvgsrlemoffres  7622  caucvgsr  7624  axpre-ltirr  7704  axpre-ltadd  7708  axpre-mulgt0  7709  axpre-mulext  7710  axcaucvglemcau  7720  axcaucvglemres  7721  ltadd2  8195  ltadd1  8205  leadd2  8207  reapval  8352  reapmul1  8371  remulext2  8376  apreim  8379  apirr  8381  apsym  8382  apcotr  8383  apadd1  8384  apadd2  8385  apneg  8387  mulext1  8388  mulext2  8389  apti  8398  apsub1  8418  subap0  8419  apmul1  8562  apmul2  8563  apdivmuld  8587  ltmul2  8628  lemul2  8629  ltdiv1  8640  ltdiv2  8659  ledivdiv  8662  lediv2  8663  negiso  8727  div4p1lem1div2  8987  qapne  9445  nn0ledivnn  9568  xleadd1  9672  xltadd1  9673  xltadd2  9674  xsubge0  9678  xleaddadd  9684  qtri3or  10034  frecfzennn  10213  monoord  10263  monoord2  10264  leexp1a  10362  bernneq  10426  nn0le2msqd  10479  faclbnd  10501  faclbnd3  10503  faclbnd6  10504  facubnd  10505  fihashdom  10563  zfz1isolemiso  10596  cjap  10692  cvg1nlemcau  10770  cvg1nlemres  10771  resqrexlemlo  10799  resqrexlemcalc3  10802  absext  10849  xrnegiso  11045  xrminltinf  11055  fsumabs  11248  cvgratnnlemnexp  11307  cvgratnnlemmn  11308  addmodlteqALT  11570  nn0seqcvgd  11735  algcvg  11742  algcvga  11745  eucalgcvga  11752  qnumgt0  11889  ctinfomlemom  11953  ispsmet  12508  psmettri2  12513  ismet  12529  isxmet  12530  xmettri2  12546  blvalps  12573  blval  12574  comet  12684  bdxmet  12686  dvef  12873  cxplt  13017  rpcxple2  13019  rpcxplt2  13020  cxplt3  13021  apdifflemr  13349  apdiff  13350
  Copyright terms: Public domain W3C validator