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

Theorem breq1d 3802
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
breq1d  |-  ( ph  ->  ( A R C  <-> 
B R C ) )

Proof of Theorem breq1d
StepHypRef Expression
1 breq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 breq1 3795 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
31, 2syl 14 1  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102    = wceq 1259   class class class wbr 3792
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-un 2950  df-sn 3409  df-pr 3410  df-op 3412  df-br 3793
This theorem is referenced by:  eqbrtrd  3812  syl6eqbr  3829  sbcbr2g  3844  pofun  4077  fmptco  5358  isorel  5476  isocnv  5479  isotr  5484  caovordig  5694  caovordg  5696  caovord  5700  xporderlem  5880  reldmtpos  5899  brtposg  5900  tpostpos  5910  tposoprab  5926  th3qlem2  6240  ensn1g  6308  fndmeng  6320  xpsneng  6327  xpcomco  6331  snnen2oprc  6354  ltsonq  6554  ltanqg  6556  ltmnqg  6557  archnqq  6573  prloc  6647  addnqprulem  6684  appdivnq  6719  mulnqpru  6725  mullocprlem  6726  1idpru  6747  cauappcvgprlemm  6801  cauappcvgprlemopl  6802  cauappcvgprlemlol  6803  cauappcvgprlemdisj  6807  cauappcvgprlemloc  6808  cauappcvgprlemladdfl  6811  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  cauappcvgprlem1  6815  cauappcvgprlem2  6816  cauappcvgprlemlim  6817  cauappcvgpr  6818  caucvgprlemnkj  6822  caucvgprlemnbj  6823  caucvgprlemm  6824  caucvgprlemopl  6825  caucvgprlemlol  6826  caucvgprlemdisj  6830  caucvgprlemloc  6831  caucvgprlemcl  6832  caucvgprlemladdfu  6833  caucvgprlemladdrl  6834  caucvgprlem1  6835  caucvgprlem2  6836  caucvgpr  6838  caucvgprprlemell  6841  caucvgprprlemelu  6842  caucvgprprlemcbv  6843  caucvgprprlemval  6844  caucvgprprlemnkltj  6845  caucvgprprlemnkeqj  6846  caucvgprprlemnbj  6849  caucvgprprlemml  6850  caucvgprprlemmu  6851  caucvgprprlemopl  6853  caucvgprprlemlol  6854  caucvgprprlemopu  6855  caucvgprprlemloc  6859  caucvgprprlemclphr  6861  caucvgprprlemexbt  6862  caucvgprprlemexb  6863  caucvgprprlemaddq  6864  caucvgprprlem1  6865  caucvgprprlem2  6866  ltsosr  6907  ltasrg  6913  addgt0sr  6918  mulextsr1  6923  prsrlt  6929  caucvgsrlemgt1  6937  caucvgsrlemoffres  6942  caucvgsr  6944  pitonnlem2  6981  pitonn  6982  recidpipr  6990  axpre-ltadd  7018  axpre-mulext  7020  nntopi  7026  axcaucvglemval  7029  axcaucvglemcau  7030  axcaucvglemres  7031  ltaddnegr  7494  ltsubadd  7501  lesubadd  7503  ltaddsub2  7506  leaddsub2  7508  ltaddpos  7521  lesub2  7526  ltsub2  7528  ltnegcon2  7533  lenegcon2  7536  addge01  7541  subge0  7544  suble0  7545  lesub0  7548  apreap  7652  divap0b  7736  mulgt1  7904  ltmulgt11  7905  gt0div  7911  ge0div  7912  ltmuldiv  7915  ltmuldiv2  7916  lemuldiv2  7923  ltrec  7924  lerec2  7930  ltdiv23  7933  lediv23  7934  addltmul  8218  avglt1  8220  avgle1  8222  div4p1lem1div2  8235  ztri3or  8345  zlem1lt  8358  zgt0ge1  8360  qapne  8671  divlt1lt  8748  divle1le  8749  xrltso  8818  xltnegi  8849  nn0disj  9097  qavgle  9215  frec2uzf1od  9356  expivallem  9421  expap0  9450  leexp2r  9474  sqap0  9486  nn0opthlem1d  9588  shftfvalg  9647  shftfibg  9649  shftfval  9650  shftfib  9652  shftfn  9653  2shfti  9660  shftidt2  9661  caucvgre  9808  cvg1nlemcau  9811  cvg1nlemres  9812  resqrexlemdecn  9839  resqrexlemoverl  9848  resqrexlemglsq  9849  resqrexlemsqa  9851  resqrexlemex  9852  abs00ap  9889  absdiflt  9919  absdifle  9920  lenegsq  9922  cau3lem  9941  clim  10033  clim2  10035  clim0  10037  clim0c  10038  climi0  10041  climuni  10045  2clim  10053  climshftlemg  10054  climshft  10056  climabs0  10059  climcn1  10060  climcn2  10061  addcn2  10062  subcn2  10063  mulcn2  10064  climcau  10097  serif0  10102  sumeq1  10105  halfleoddlt  10206  pw2dvdslemn  10253  pw2dvdseu  10256  oddpwdclemxy  10257  oddpwdclemndvds  10259  oddpwdclemodd  10260  qdencn  10511
  Copyright terms: Public domain W3C validator