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

Theorem breq1d 3909
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 3902 . 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 104    = wceq 1316   class class class wbr 3899
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-br 3900
This theorem is referenced by:  eqbrtrd  3920  eqbrtrdi  3937  sbcbr2g  3955  pofun  4204  fmptco  5554  isorel  5677  isocnv  5680  isotr  5685  imbrov2fvoveq  5767  caovordig  5904  caovordg  5906  caovord  5910  xporderlem  6096  reldmtpos  6118  brtposg  6119  tpostpos  6129  tposoprab  6145  th3qlem2  6500  ensn1g  6659  fndmeng  6672  xpsneng  6684  xpcomco  6688  snnen2oprc  6722  tridc  6761  fimax2gtrilemstep  6762  unsnfidcel  6777  pm54.43  7014  ccfunen  7047  ltsonq  7174  ltanqg  7176  ltmnqg  7177  archnqq  7193  prloc  7267  addnqprulem  7304  appdivnq  7339  mulnqpru  7345  mullocprlem  7346  1idpru  7367  cauappcvgprlemm  7421  cauappcvgprlemopl  7422  cauappcvgprlemlol  7423  cauappcvgprlemdisj  7427  cauappcvgprlemloc  7428  cauappcvgprlemladdfl  7431  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  cauappcvgprlem1  7435  cauappcvgprlem2  7436  cauappcvgprlemlim  7437  cauappcvgpr  7438  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemlol  7446  caucvgprlemdisj  7450  caucvgprlemloc  7451  caucvgprlemcl  7452  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  caucvgprlem1  7455  caucvgprlem2  7456  caucvgpr  7458  caucvgprprlemell  7461  caucvgprprlemelu  7462  caucvgprprlemcbv  7463  caucvgprprlemval  7464  caucvgprprlemnkltj  7465  caucvgprprlemnkeqj  7466  caucvgprprlemnbj  7469  caucvgprprlemml  7470  caucvgprprlemmu  7471  caucvgprprlemopl  7473  caucvgprprlemlol  7474  caucvgprprlemopu  7475  caucvgprprlemloc  7479  caucvgprprlemclphr  7481  caucvgprprlemexbt  7482  caucvgprprlemexb  7483  caucvgprprlemaddq  7484  caucvgprprlem1  7485  caucvgprprlem2  7486  ltsosr  7540  ltasrg  7546  addgt0sr  7551  mulextsr1  7557  prsrlt  7563  caucvgsrlemgt1  7571  caucvgsrlemoffres  7576  caucvgsr  7578  ltpsrprg  7579  pitonnlem2  7623  pitonn  7624  recidpipr  7632  axpre-ltadd  7662  axpre-mulext  7664  nntopi  7670  axcaucvglemval  7673  axcaucvglemcau  7674  axcaucvglemres  7675  ltaddnegr  8155  ltsubadd  8162  lesubadd  8164  ltaddsub2  8167  leaddsub2  8169  ltaddpos  8182  lesub2  8187  ltsub2  8189  ltnegcon2  8194  lenegcon2  8197  addge01  8202  subge0  8205  suble0  8206  lesub0  8209  ltordlem  8212  apreap  8317  divap0b  8411  mulgt1  8589  ltmulgt11  8590  gt0div  8596  ge0div  8597  ltmuldiv  8600  ltmuldiv2  8601  lemuldiv2  8608  ltrec  8609  lerec2  8615  ltdiv23  8618  lediv23  8619  sup3exmid  8683  addltmul  8924  avglt1  8926  avgle1  8928  div4p1lem1div2  8941  ztri3or  9065  zlem1lt  9078  zgt0ge1  9080  qapne  9399  divlt1lt  9479  divle1le  9480  xrltso  9550  xltnegi  9586  xltadd1  9627  xposdif  9633  xlesubadd  9634  xleaddadd  9638  nn0disj  9883  qavgle  10004  frec2uzf1od  10147  iseqf1olemfvp  10238  exp3vallem  10262  expap0  10291  leexp2r  10315  sqap0  10327  nn0opthlem1d  10434  hashennnuni  10493  hashunlem  10518  zfz1isolemiso  10550  seq3coll  10553  shftfvalg  10558  shftfibg  10560  shftfval  10561  shftfib  10563  shftfn  10564  2shfti  10571  shftidt2  10572  caucvgre  10721  cvg1nlemcau  10724  cvg1nlemres  10725  resqrexlemdecn  10752  resqrexlemoverl  10761  resqrexlemglsq  10762  resqrexlemsqa  10764  resqrexlemex  10765  abs00ap  10802  absdiflt  10832  absdifle  10833  lenegsq  10835  cau3lem  10854  minmax  10969  xrmaxltsup  10995  xrminmax  11002  xrltmininf  11007  xrlemininf  11008  clim  11018  clim2  11020  clim0  11022  clim0c  11023  climi0  11026  climuni  11030  2clim  11038  climshftlemg  11039  climshft  11041  climabs0  11044  climcn1  11045  climcn2  11046  addcn2  11047  subcn2  11048  mulcn2  11049  iser3shft  11083  climcau  11084  serf0  11089  sumeq1  11092  sumeq2  11096  sumrbdc  11115  summodclem2  11119  summodc  11120  zsumdc  11121  isumshft  11227  mertenslemi1  11272  mertenslem2  11273  mertensabs  11274  tanaddaplem  11372  sin01bnd  11391  cos01bnd  11392  halfleoddlt  11518  gcddvds  11579  dvdssq  11646  lcmgcdlem  11685  lcmdvds  11687  isprm  11717  prmgt1  11739  isprm6  11752  pw2dvdslemn  11770  pw2dvdseu  11773  oddpwdclemxy  11774  oddpwdclemndvds  11776  oddpwdclemodd  11777  blfvalps  12481  elblps  12486  elbl  12487  elbl3ps  12490  elbl3  12491  blres  12530  comet  12595  bdbl  12599  xmetxp  12603  xmetxpbl  12604  metcnp2  12609  txmetcnp  12614  cnbl0  12630  cnblcld  12631  bl2ioo  12638  addcncntoplem  12647  divcnap  12651  elcncf  12656  elcncf2  12657  cncfi  12661  rescncf  12664  mulc1cncf  12672  cncfco  12674  cncfmet  12675  cncfmptid  12679  addccncf  12682  cdivcncfap  12683  negcncf  12684  mulcncflem  12686  mulcncf  12687  ivthinclemlm  12708  ivthinclemlopn  12710  ivthinclemlr  12711  ivthinclemuopn  12712  ivthinclemur  12713  ivthinclemdisj  12714  ivthinclemloc  12715  ivthinc  12717  limccl  12724  ellimc3apf  12725  limcdifap  12727  limcmpted  12728  limcimolemlt  12729  limcresi  12731  cnplimcim  12732  limccnpcntop  12740  limccnp2lem  12741  limccoap  12743  dvcoapbr  12767  dveflem  12782  sincosq2sgn  12835  sincosq3sgn  12836  sincosq4sgn  12837  qdencn  13149  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator