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

Theorem breq12d 4043
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 4035 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2anc 411 1  |-  ( ph  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105    = wceq 1364   class class class wbr 4030
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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-br 4031
This theorem is referenced by:  breq123d  4044  3brtr3d  4061  3brtr4d  4062  pocl  4335  csbcnvg  4847  cnvpom  5209  sbcfung  5279  isoeq1  5845  isocnv  5855  isotr  5860  caovordig  6086  caovordg  6088  caovord2d  6090  caovord  6092  ofrfval  6141  ofrval  6143  ofrfval2  6149  caofref  6156  fundmeng  6863  xpsneng  6878  xpcomeng  6884  xpdom2g  6888  phplem3g  6914  php5  6916  php5dom  6921  exmidpw2en  6970  exmidapne  7322  nqtri3or  7458  ltsonq  7460  ltanqg  7462  ltmnqg  7463  lt2addnq  7466  lt2mulnq  7467  prarloclemarch  7480  ltrnqg  7482  ltnnnq  7485  prarloclemlt  7555  addlocprlemgt  7596  mullocprlem  7632  addextpr  7683  recexprlemss1l  7697  recexprlemss1u  7698  recexpr  7700  caucvgprlemcanl  7706  cauappcvgprlemm  7707  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem1  7721  cauappcvgprlemlim  7723  cauappcvgpr  7724  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemcl  7738  caucvgprlemladdrl  7740  caucvgprlem1  7741  caucvgpr  7744  caucvgprprlemell  7747  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemnkeqj  7752  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemloc  7765  caucvgprprlemclphr  7767  caucvgprprlemexb  7769  caucvgprprlem1  7771  lttrsr  7824  ltposr  7825  ltsosr  7826  ltasrg  7832  aptisr  7841  mulextsr1lem  7842  mulextsr1  7843  caucvgsrlemcau  7855  caucvgsrlemgt1  7857  caucvgsrlemoffcau  7860  caucvgsrlemoffres  7862  caucvgsr  7864  axpre-ltirr  7944  axpre-ltadd  7948  axpre-mulgt0  7949  axpre-mulext  7950  axcaucvglemcau  7960  axcaucvglemres  7961  ltadd2  8440  ltadd1  8450  leadd2  8452  reapval  8597  reapmul1  8616  remulext2  8621  apreim  8624  apirr  8626  apsym  8627  apcotr  8628  apadd1  8629  apadd2  8630  apneg  8632  mulext1  8633  mulext2  8634  apti  8643  apsub1  8663  subap0  8664  apmul1  8809  apmul2  8810  apdivmuld  8834  ltmul2  8877  lemul2  8878  ltdiv1  8889  ltdiv2  8908  ledivdiv  8911  lediv2  8912  negiso  8976  div4p1lem1div2  9239  qapne  9707  nn0ledivnn  9836  xleadd1  9944  xltadd1  9945  xltadd2  9946  xsubge0  9950  xleaddadd  9956  qtri3or  10313  frecfzennn  10500  monoord  10559  monoord2  10560  leexp1a  10668  bernneq  10734  apexp1  10792  nn0le2msqd  10793  faclbnd  10815  faclbnd3  10817  faclbnd6  10818  facubnd  10819  fihashdom  10877  zfz1isolemiso  10913  cjap  11053  cvg1nlemcau  11131  cvg1nlemres  11132  resqrexlemlo  11160  resqrexlemcalc3  11163  absext  11210  xrnegiso  11408  xrminltinf  11418  fsumabs  11611  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  fprodle  11786  addmodlteqALT  12004  nn0seqcvgd  12182  algcvg  12189  algcvga  12192  eucalgcvga  12199  qnumgt0  12339  pcprendvds2  12432  pcpremul  12434  pcadd2  12482  ctinfomlemom  12587  gsumfzval  12977  ispsmet  14502  psmettri2  14507  ismet  14523  isxmet  14524  xmettri2  14540  blvalps  14567  blval  14568  comet  14678  bdxmet  14680  dvef  14906  cxplt  15091  rpcxple2  15093  rpcxplt2  15094  cxplt3  15095  apcxp2  15113  ltexp2  15115  logbleb  15134  logblt  15135  lgsdilem  15184  2lgslem1a2  15244  apdifflemr  15607  apdiff  15608
  Copyright terms: Public domain W3C validator