Theorem breq1d 4044

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   class class class wbr 4034

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  eqnbrtrd  4052  eqbrtrd  4056  eqbrtrdi  4073  sbcbr2g  4091  pofun  4348  fmptco  5731  isorel  5858  isocnv  5861  isotr  5866  imbrov2fvoveq  5950  caovordig  6093  caovordg  6095  caovord  6099  xporderlem  6298  reldmtpos  6320  brtposg  6321  tpostpos  6331  tposoprab  6347  th3qlem2  6706  ensn1g  6865  fndmeng  6878  xpsneng  6890  xpcomco  6894  snnen2oprc  6930  tridc  6969  fimax2gtrilemstep  6970  unsnfidcel  6991  pm54.43  7269  ccfunen  7347  ltsonq  7482  ltanqg  7484  ltmnqg  7485  archnqq  7501  prloc  7575  addnqprulem  7612  appdivnq  7647  mulnqpru  7653  mullocprlem  7654  1idpru  7675  cauappcvgprlemm  7729  cauappcvgprlemopl  7730  cauappcvgprlemlol  7731  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlemladdfl  7739  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem1  7743  cauappcvgprlem2  7744  cauappcvgprlemlim  7745  cauappcvgpr  7746  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlemcl  7760  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  caucvgprlem1  7763  caucvgprlem2  7764  caucvgpr  7766  caucvgprprlemell  7769  caucvgprprlemelu  7770  caucvgprprlemcbv  7771  caucvgprprlemval  7772  caucvgprprlemnkltj  7773  caucvgprprlemnkeqj  7774  caucvgprprlemnbj  7777  caucvgprprlemml  7778  caucvgprprlemmu  7779  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemopu  7783  caucvgprprlemloc  7787  caucvgprprlemclphr  7789  caucvgprprlemexbt  7790  caucvgprprlemexb  7791  caucvgprprlemaddq  7792  caucvgprprlem1  7793  caucvgprprlem2  7794  ltsosr  7848  ltasrg  7854  addgt0sr  7859  mulextsr1  7865  prsrlt  7871  caucvgsrlemgt1  7879  caucvgsrlemoffres  7884  caucvgsr  7886  ltpsrprg  7887  pitonnlem2  7931  pitonn  7932  recidpipr  7940  axpre-ltadd  7970  axpre-mulext  7972  nntopi  7978  axcaucvglemval  7981  axcaucvglemcau  7982  axcaucvglemres  7983  ltaddnegr  8469  ltsubadd  8476  lesubadd  8478  ltaddsub2  8481  leaddsub2  8483  ltaddpos  8496  lesub2  8501  ltsub2  8503  ltnegcon2  8508  lenegcon2  8511  addge01  8516  subge0  8519  suble0  8520  lesub0  8523  ltordlem  8526  apreap  8631  divap0b  8727  mulgt1  8907  ltmulgt11  8908  gt0div  8914  ge0div  8915  ltmuldiv  8918  ltmuldiv2  8919  lemuldiv2  8926  ltrec  8927  lerec2  8933  ltdiv23  8936  lediv23  8937  sup3exmid  9001  addltmul  9245  avglt1  9247  avgle1  9249  div4p1lem1div2  9262  ztri3or  9386  zlem1lt  9399  zgt0ge1  9401  qapne  9730  irrmulap  9739  divlt1lt  9816  divle1le  9817  xrltso  9888  xltnegi  9927  xltadd1  9968  xposdif  9974  xlesubadd  9975  xleaddadd  9979  nn0disj  10230  qavgle  10365  fldiv4lem1div2uz2  10413  frec2uzf1od  10515  iseqf1olemfvp  10619  seqf1oglem1  10628  exp3vallem  10649  expap0  10678  leexp2r  10702  sqap0  10715  nn0ltexp2  10818  nn0opthlem1d  10829  hashennnuni  10888  hashunlem  10913  zfz1isolemiso  10948  seq3coll  10951  shftfvalg  11000  shftfibg  11002  shftfval  11003  shftfib  11005  shftfn  11006  2shfti  11013  shftidt2  11014  caucvgre  11163  cvg1nlemcau  11166  cvg1nlemres  11167  resqrexlemdecn  11194  resqrexlemoverl  11203  resqrexlemglsq  11204  resqrexlemsqa  11206  resqrexlemex  11207  abs00ap  11244  absdiflt  11274  absdifle  11275  lenegsq  11277  cau3lem  11296  minmax  11412  xrmaxltsup  11440  xrminmax  11447  xrltmininf  11452  xrlemininf  11453  clim  11463  clim2  11465  clim0  11467  clim0c  11468  climi0  11471  climuni  11475  2clim  11483  climshftlemg  11484  climshft  11486  climabs0  11489  climcn1  11490  climcn2  11491  addcn2  11492  subcn2  11493  mulcn2  11494  iser3shft  11528  climcau  11529  serf0  11534  sumeq1  11537  sumeq2  11541  sumrbdc  11561  summodclem2  11564  summodc  11565  zsumdc  11566  isumshft  11672  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  prodfap0  11727  prodfrecap  11728  prodfdivap  11729  ntrivcvgap  11730  ntrivcvgap0  11731  prodeq1f  11734  prodeq2w  11738  prodeq2  11739  prodrbdclem2  11755  prodmodclem2  11759  prodmodc  11760  zproddc  11761  fprodntrivap  11766  fprodap0  11803  fprodrec  11811  fproddivapf  11813  fprodap0f  11818  tanaddaplem  11920  sin01bnd  11939  cos01bnd  11940  halfleoddlt  12076  gcddvds  12155  dvdssq  12223  lcmgcdlem  12270  lcmdvds  12272  isprm  12302  prmgt1  12325  isprm5lem  12334  isprm6  12340  pw2dvdslemn  12358  pw2dvdseu  12361  oddpwdclemxy  12362  oddpwdclemndvds  12364  oddpwdclemodd  12365  odzdvds  12439  pclem0  12480  pclemub  12481  pclemdc  12482  pcprecl  12483  pcprendvds  12484  pcpremul  12487  pceulem  12488  pcval  12490  pcelnn  12515  pc2dvds  12524  pcadd  12534  pcadd2  12535  pcmpt  12537  prmpwdvds  12549  4sqlem17  12601  imasaddfnlemg  13016  znf1o  14283  znidomb  14290  blfvalps  14705  elblps  14710  elbl  14711  elbl3ps  14714  elbl3  14715  blres  14754  comet  14819  bdbl  14823  xmetxp  14827  xmetxpbl  14828  metcnp2  14833  txmetcnp  14838  cnbl0  14854  cnblcld  14855  bl2ioo  14870  addcncntoplem  14881  divcnap  14885  mpomulcn  14886  elcncf  14893  elcncf2  14894  cncfi  14898  rescncf  14901  mulc1cncf  14909  cncfco  14911  cncfmet  14912  cncfmptid  14917  addccncf  14920  cdivcncfap  14924  negcncf  14925  mulcncflem  14927  mulcncf  14928  ivthinclemlm  14954  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemdisj  14960  ivthinclemloc  14961  ivthinc  14963  ivthreinc  14965  limccl  14979  ellimc3apf  14980  limcdifap  14982  limcmpted  14983  limcimolemlt  14984  limcresi  14986  cnplimcim  14987  limccnpcntop  14995  limccnp2lem  14996  limccoap  14998  dvcoapbr  15027  dveflem  15046  eflt  15095  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  logltb  15194  logge0b  15210  loggt0b  15211  lgslem2  15326  lgslem3  15327  lgsval  15329  lgsfcl2  15331  lgsfle1  15334  lgsle1  15340  lgsdirprm  15359  lgsne0  15363  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  gausslemma2dlem2  15387  gausslemma2dlem3  15388  gausslemma2dlem4  15389  qdencn  15758  trilpolemlt1  15772