Theorem breq1d 4069

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
breq1d	⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Proof of Theorem breq1d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq1 4062	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   class class class wbr 4059

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-br 4060

This theorem is referenced by:  eqnbrtrd  4077  eqbrtrd  4081  eqbrtrdi  4098  sbcbr2g  4117  pofun  4377  fmptco  5769  isorel  5900  isocnv  5903  isotr  5908  imbrov2fvoveq  5992  caovordig  6135  caovordg  6137  caovord  6141  xporderlem  6340  reldmtpos  6362  brtposg  6363  tpostpos  6373  tposoprab  6389  th3qlem2  6748  ensn1g  6912  fndmeng  6926  xpsneng  6942  xpcomco  6946  snnen2oprc  6982  tridc  7022  fimax2gtrilemstep  7023  unsnfidcel  7044  pm54.43  7324  pr1or2  7328  ccfunen  7411  ltsonq  7546  ltanqg  7548  ltmnqg  7549  archnqq  7565  prloc  7639  addnqprulem  7676  appdivnq  7711  mulnqpru  7717  mullocprlem  7718  1idpru  7739  cauappcvgprlemm  7793  cauappcvgprlemopl  7794  cauappcvgprlemlol  7795  cauappcvgprlemdisj  7799  cauappcvgprlemloc  7800  cauappcvgprlemladdfl  7803  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem1  7807  cauappcvgprlem2  7808  cauappcvgprlemlim  7809  cauappcvgpr  7810  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemm  7816  caucvgprlemopl  7817  caucvgprlemlol  7818  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemcl  7824  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  caucvgprlem1  7827  caucvgprlem2  7828  caucvgpr  7830  caucvgprprlemell  7833  caucvgprprlemelu  7834  caucvgprprlemcbv  7835  caucvgprprlemval  7836  caucvgprprlemnkltj  7837  caucvgprprlemnkeqj  7838  caucvgprprlemnbj  7841  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemopl  7845  caucvgprprlemlol  7846  caucvgprprlemopu  7847  caucvgprprlemloc  7851  caucvgprprlemclphr  7853  caucvgprprlemexbt  7854  caucvgprprlemexb  7855  caucvgprprlemaddq  7856  caucvgprprlem1  7857  caucvgprprlem2  7858  ltsosr  7912  ltasrg  7918  addgt0sr  7923  mulextsr1  7929  prsrlt  7935  caucvgsrlemgt1  7943  caucvgsrlemoffres  7948  caucvgsr  7950  ltpsrprg  7951  pitonnlem2  7995  pitonn  7996  recidpipr  8004  axpre-ltadd  8034  axpre-mulext  8036  nntopi  8042  axcaucvglemval  8045  axcaucvglemcau  8046  axcaucvglemres  8047  ltaddnegr  8533  ltsubadd  8540  lesubadd  8542  ltaddsub2  8545  leaddsub2  8547  ltaddpos  8560  lesub2  8565  ltsub2  8567  ltnegcon2  8572  lenegcon2  8575  addge01  8580  subge0  8583  suble0  8584  lesub0  8587  ltordlem  8590  apreap  8695  divap0b  8791  mulgt1  8971  ltmulgt11  8972  gt0div  8978  ge0div  8979  ltmuldiv  8982  ltmuldiv2  8983  lemuldiv2  8990  ltrec  8991  lerec2  8997  ltdiv23  9000  lediv23  9001  sup3exmid  9065  addltmul  9309  avglt1  9311  avgle1  9313  div4p1lem1div2  9326  ztri3or  9450  zlem1lt  9464  zgt0ge1  9466  qapne  9795  irrmulap  9804  divlt1lt  9881  divle1le  9882  xrltso  9953  xltnegi  9992  xltadd1  10033  xposdif  10039  xlesubadd  10040  xleaddadd  10044  nn0disj  10295  qavgle  10438  fldiv4lem1div2uz2  10486  frec2uzf1od  10588  iseqf1olemfvp  10692  seqf1oglem1  10701  exp3vallem  10722  expap0  10751  leexp2r  10775  sqap0  10788  nn0ltexp2  10891  nn0opthlem1d  10902  hashennnuni  10961  hashunlem  10986  zfz1isolemiso  11021  seq3coll  11024  swrdccatin2  11220  shftfvalg  11244  shftfibg  11246  shftfval  11247  shftfib  11249  shftfn  11250  2shfti  11257  shftidt2  11258  caucvgre  11407  cvg1nlemcau  11410  cvg1nlemres  11411  resqrexlemdecn  11438  resqrexlemoverl  11447  resqrexlemglsq  11448  resqrexlemsqa  11450  resqrexlemex  11451  abs00ap  11488  absdiflt  11518  absdifle  11519  lenegsq  11521  cau3lem  11540  minmax  11656  xrmaxltsup  11684  xrminmax  11691  xrltmininf  11696  xrlemininf  11697  clim  11707  clim2  11709  clim0  11711  clim0c  11712  climi0  11715  climuni  11719  2clim  11727  climshftlemg  11728  climshft  11730  climabs0  11733  climcn1  11734  climcn2  11735  addcn2  11736  subcn2  11737  mulcn2  11738  iser3shft  11772  climcau  11773  serf0  11778  sumeq1  11781  sumeq2  11785  sumrbdc  11805  summodclem2  11808  summodc  11809  zsumdc  11810  isumshft  11916  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  prodfap0  11971  prodfrecap  11972  prodfdivap  11973  ntrivcvgap  11974  ntrivcvgap0  11975  prodeq1f  11978  prodeq2w  11982  prodeq2  11983  prodrbdclem2  11999  prodmodclem2  12003  prodmodc  12004  zproddc  12005  fprodntrivap  12010  fprodap0  12047  fprodrec  12055  fproddivapf  12057  fprodap0f  12062  tanaddaplem  12164  sin01bnd  12183  cos01bnd  12184  halfleoddlt  12320  gcddvds  12399  dvdssq  12467  lcmgcdlem  12514  lcmdvds  12516  isprm  12546  prmgt1  12569  isprm5lem  12578  isprm6  12584  pw2dvdslemn  12602  pw2dvdseu  12605  oddpwdclemxy  12606  oddpwdclemndvds  12608  oddpwdclemodd  12609  odzdvds  12683  pclem0  12724  pclemub  12725  pclemdc  12726  pcprecl  12727  pcprendvds  12728  pcpremul  12731  pceulem  12732  pcval  12734  pcelnn  12759  pc2dvds  12768  pcadd  12778  pcadd2  12779  pcmpt  12781  prmpwdvds  12793  4sqlem17  12845  imasaddfnlemg  13261  znf1o  14528  znidomb  14535  mplsubgfilemm  14575  mplsubgfilemcl  14576  blfvalps  14972  elblps  14977  elbl  14978  elbl3ps  14981  elbl3  14982  blres  15021  comet  15086  bdbl  15090  xmetxp  15094  xmetxpbl  15095  metcnp2  15100  txmetcnp  15105  cnbl0  15121  cnblcld  15122  bl2ioo  15137  addcncntoplem  15148  divcnap  15152  mpomulcn  15153  elcncf  15160  elcncf2  15161  cncfi  15165  rescncf  15168  mulc1cncf  15176  cncfco  15178  cncfmet  15179  cncfmptid  15184  addccncf  15187  cdivcncfap  15191  negcncf  15192  mulcncflem  15194  mulcncf  15195  ivthinclemlm  15221  ivthinclemlopn  15223  ivthinclemlr  15224  ivthinclemuopn  15225  ivthinclemur  15226  ivthinclemdisj  15227  ivthinclemloc  15228  ivthinc  15230  ivthreinc  15232  limccl  15246  ellimc3apf  15247  limcdifap  15249  limcmpted  15250  limcimolemlt  15251  limcresi  15253  cnplimcim  15254  limccnpcntop  15262  limccnp2lem  15263  limccoap  15265  dvcoapbr  15294  dveflem  15313  eflt  15362  sincosq2sgn  15414  sincosq3sgn  15415  sincosq4sgn  15416  logltb  15461  logge0b  15477  loggt0b  15478  lgslem2  15593  lgslem3  15594  lgsval  15596  lgsfcl2  15598  lgsfle1  15601  lgsle1  15607  lgsdirprm  15626  lgsne0  15630  gausslemma2dlem1a  15650  gausslemma2dlem1f1o  15652  gausslemma2dlem2  15654  gausslemma2dlem3  15655  gausslemma2dlem4  15656  qdencn  16168  trilpolemlt1  16182