Theorem breq1d 4119

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 4112	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   class class class wbr 4109

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110

This theorem is referenced by:  eqnbrtrd  4127  eqbrtrd  4131  eqbrtrdi  4148  sbcbr2g  4167  pofun  4433  fmptco  5843  isorel  5981  isocnv  5984  isotr  5989  imbrov2fvoveq  6075  caovordig  6220  caovordg  6222  caovord  6226  xporderlem  6427  reldmtpos  6484  brtposg  6485  tpostpos  6495  tposoprab  6511  th3qlem2  6872  ensn1g  7037  fndmeng  7051  xpsneng  7073  xpcomco  7077  snnen2oprc  7114  tridc  7157  fimax2gtrilemstep  7158  unsnfidcel  7181  pm54.43  7487  pr1or2  7491  ccfunen  7578  ltsonq  7713  ltanqg  7715  ltmnqg  7716  archnqq  7732  prloc  7806  addnqprulem  7843  appdivnq  7878  mulnqpru  7884  mullocprlem  7885  1idpru  7906  cauappcvgprlemm  7960  cauappcvgprlemopl  7961  cauappcvgprlemlol  7962  cauappcvgprlemdisj  7966  cauappcvgprlemloc  7967  cauappcvgprlemladdfl  7970  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  cauappcvgprlem1  7974  cauappcvgprlem2  7975  cauappcvgprlemlim  7976  cauappcvgpr  7977  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemm  7983  caucvgprlemopl  7984  caucvgprlemlol  7985  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprlemcl  7991  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  caucvgprlem1  7994  caucvgprlem2  7995  caucvgpr  7997  caucvgprprlemell  8000  caucvgprprlemelu  8001  caucvgprprlemcbv  8002  caucvgprprlemval  8003  caucvgprprlemnkltj  8004  caucvgprprlemnkeqj  8005  caucvgprprlemnbj  8008  caucvgprprlemml  8009  caucvgprprlemmu  8010  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemopu  8014  caucvgprprlemloc  8018  caucvgprprlemclphr  8020  caucvgprprlemexbt  8021  caucvgprprlemexb  8022  caucvgprprlemaddq  8023  caucvgprprlem1  8024  caucvgprprlem2  8025  ltsosr  8079  ltasrg  8085  addgt0sr  8090  mulextsr1  8096  prsrlt  8102  caucvgsrlemgt1  8110  caucvgsrlemoffres  8115  caucvgsr  8117  ltpsrprg  8118  pitonnlem2  8162  pitonn  8163  recidpipr  8171  axpre-ltadd  8201  axpre-mulext  8203  nntopi  8209  axcaucvglemval  8212  axcaucvglemcau  8213  axcaucvglemres  8214  ltaddnegr  8699  ltsubadd  8706  lesubadd  8708  ltaddsub2  8711  leaddsub2  8713  ltaddpos  8726  lesub2  8731  ltsub2  8733  ltnegcon2  8738  lenegcon2  8741  addge01  8746  subge0  8749  suble0  8750  lesub0  8753  ltordlem  8756  apreap  8861  divap0b  8957  mulgt1  9137  ltmulgt11  9138  gt0div  9144  ge0div  9145  ltmuldiv  9148  ltmuldiv2  9149  lemuldiv2  9156  ltrec  9157  lerec2  9163  ltdiv23  9166  lediv23  9167  sup3exmid  9231  addltmul  9475  avglt1  9477  avgle1  9479  div4p1lem1div2  9492  ztri3or  9620  zlem1lt  9634  zgt0ge1  9636  qapne  9971  irrmulap  9980  divlt1lt  10057  divle1le  10058  xrltso  10129  xltnegi  10168  xltadd1  10209  xposdif  10215  xlesubadd  10216  xleaddadd  10220  nn0disj  10472  qavgle  10618  fldiv4lem1div2uz2  10666  frec2uzf1od  10768  iseqf1olemfvp  10872  seqf1oglem1  10881  exp3vallem  10902  expap0  10931  leexp2r  10955  sqap0  10968  nn0ltexp2  11071  nn0opthlem1d  11082  hashennnuni  11142  hashunlem  11168  zfz1isolemiso  11211  seq3coll  11214  swrdccatin2  11421  shftfvalg  11503  shftfibg  11505  shftfval  11506  shftfib  11508  shftfn  11509  2shfti  11516  shftidt2  11517  caucvgre  11666  cvg1nlemcau  11669  cvg1nlemres  11670  resqrexlemdecn  11697  resqrexlemoverl  11706  resqrexlemglsq  11707  resqrexlemsqa  11709  resqrexlemex  11710  abs00ap  11747  absdiflt  11777  absdifle  11778  lenegsq  11780  cau3lem  11799  minmax  11915  xrmaxltsup  11943  xrminmax  11950  xrltmininf  11955  xrlemininf  11956  clim  11966  clim2  11968  clim0  11970  clim0c  11971  climi0  11974  climuni  11978  2clim  11986  climshftlemg  11987  climshft  11989  climabs0  11992  climcn1  11993  climcn2  11994  addcn2  11995  subcn2  11996  mulcn2  11997  iser3shft  12031  climcau  12032  serf0  12037  sumeq1  12040  sumeq2  12044  sumrbdc  12065  summodclem2  12068  summodc  12069  zsumdc  12070  isumshft  12176  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  prodfap0  12231  prodfrecap  12232  prodfdivap  12233  ntrivcvgap  12234  ntrivcvgap0  12235  prodeq1f  12238  prodeq2w  12242  prodeq2  12243  prodrbdclem2  12259  prodmodclem2  12263  prodmodc  12264  zproddc  12265  fprodntrivap  12270  fprodap0  12307  fprodrec  12315  fproddivapf  12317  fprodap0f  12322  tanaddaplem  12424  sin01bnd  12443  cos01bnd  12444  halfleoddlt  12580  gcddvds  12659  dvdssq  12727  lcmgcdlem  12774  lcmdvds  12776  isprm  12806  prmgt1  12829  isprm5lem  12838  isprm6  12844  pw2dvdslemn  12862  pw2dvdseu  12865  oddpwdclemxy  12866  oddpwdclemndvds  12868  oddpwdclemodd  12869  odzdvds  12943  pclem0  12984  pclemub  12985  pclemdc  12986  pcprecl  12987  pcprendvds  12988  pcpremul  12991  pceulem  12992  pcval  12994  pcelnn  13019  pc2dvds  13028  pcadd  13038  pcadd2  13039  pcmpt  13041  prmpwdvds  13053  4sqlem17  13105  imasaddfnlemg  13527  znf1o  14799  znidomb  14806  mplsubgfilemm  14853  mplsubgfilemcl  14854  blfvalps  15250  elblps  15255  elbl  15256  elbl3ps  15259  elbl3  15260  blres  15299  comet  15364  bdbl  15368  xmetxp  15372  xmetxpbl  15373  metcnp2  15378  txmetcnp  15383  cnbl0  15399  cnblcld  15400  bl2ioo  15415  addcncntoplem  15426  divcnap  15430  mpomulcn  15431  elcncf  15438  elcncf2  15439  cncfi  15443  rescncf  15446  mulc1cncf  15454  cncfco  15456  cncfmet  15457  cncfmptid  15462  addccncf  15465  cdivcncfap  15469  negcncf  15470  mulcncflem  15472  mulcncf  15473  ivthinclemlm  15499  ivthinclemlopn  15501  ivthinclemlr  15502  ivthinclemuopn  15503  ivthinclemur  15504  ivthinclemdisj  15505  ivthinclemloc  15506  ivthinc  15508  ivthreinc  15510  limccl  15524  ellimc3apf  15525  limcdifap  15527  limcmpted  15528  limcimolemlt  15529  limcresi  15531  cnplimcim  15532  limccnpcntop  15540  limccnp2lem  15541  limccoap  15543  dvcoapbr  15572  dveflem  15591  eflt  15640  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  logltb  15739  logge0b  15755  loggt0b  15756  pellexlem3  15847  lgslem2  15874  lgslem3  15875  lgsval  15877  lgsfcl2  15879  lgsfle1  15882  lgsle1  15888  lgsdirprm  15907  lgsne0  15911  gausslemma2dlem1a  15931  gausslemma2dlem1f1o  15933  gausslemma2dlem2  15935  gausslemma2dlem3  15936  gausslemma2dlem4  15937  subupgr  16268  vtxdumgrfival  16293  qdencn  16807  trilpolemlt1  16825