Theorem breq1d 4013

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   class class class wbr 4003

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004

This theorem is referenced by:  eqnbrtrd  4021  eqbrtrd  4025  eqbrtrdi  4042  sbcbr2g  4060  pofun  4312  fmptco  5682  isorel  5808  isocnv  5811  isotr  5816  imbrov2fvoveq  5899  caovordig  6039  caovordg  6041  caovord  6045  xporderlem  6231  reldmtpos  6253  brtposg  6254  tpostpos  6264  tposoprab  6280  th3qlem2  6637  ensn1g  6796  fndmeng  6809  xpsneng  6821  xpcomco  6825  snnen2oprc  6859  tridc  6898  fimax2gtrilemstep  6899  unsnfidcel  6919  pm54.43  7188  ccfunen  7262  ltsonq  7396  ltanqg  7398  ltmnqg  7399  archnqq  7415  prloc  7489  addnqprulem  7526  appdivnq  7561  mulnqpru  7567  mullocprlem  7568  1idpru  7589  cauappcvgprlemm  7643  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemdisj  7649  cauappcvgprlemloc  7650  cauappcvgprlemladdfl  7653  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  cauappcvgprlem1  7657  cauappcvgprlem2  7658  cauappcvgprlemlim  7659  cauappcvgpr  7660  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemcl  7674  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgprlem1  7677  caucvgprlem2  7678  caucvgpr  7680  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnkltj  7687  caucvgprprlemnkeqj  7688  caucvgprprlemnbj  7691  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemloc  7701  caucvgprprlemclphr  7703  caucvgprprlemexbt  7704  caucvgprprlemexb  7705  caucvgprprlemaddq  7706  caucvgprprlem1  7707  caucvgprprlem2  7708  ltsosr  7762  ltasrg  7768  addgt0sr  7773  mulextsr1  7779  prsrlt  7785  caucvgsrlemgt1  7793  caucvgsrlemoffres  7798  caucvgsr  7800  ltpsrprg  7801  pitonnlem2  7845  pitonn  7846  recidpipr  7854  axpre-ltadd  7884  axpre-mulext  7886  nntopi  7892  axcaucvglemval  7895  axcaucvglemcau  7896  axcaucvglemres  7897  ltaddnegr  8381  ltsubadd  8388  lesubadd  8390  ltaddsub2  8393  leaddsub2  8395  ltaddpos  8408  lesub2  8413  ltsub2  8415  ltnegcon2  8420  lenegcon2  8423  addge01  8428  subge0  8431  suble0  8432  lesub0  8435  ltordlem  8438  apreap  8543  divap0b  8639  mulgt1  8819  ltmulgt11  8820  gt0div  8826  ge0div  8827  ltmuldiv  8830  ltmuldiv2  8831  lemuldiv2  8838  ltrec  8839  lerec2  8845  ltdiv23  8848  lediv23  8849  sup3exmid  8913  addltmul  9154  avglt1  9156  avgle1  9158  div4p1lem1div2  9171  ztri3or  9295  zlem1lt  9308  zgt0ge1  9310  qapne  9638  divlt1lt  9723  divle1le  9724  xrltso  9795  xltnegi  9834  xltadd1  9875  xposdif  9881  xlesubadd  9882  xleaddadd  9886  nn0disj  10137  qavgle  10258  frec2uzf1od  10405  iseqf1olemfvp  10496  exp3vallem  10520  expap0  10549  leexp2r  10573  sqap0  10586  nn0ltexp2  10688  nn0opthlem1d  10699  hashennnuni  10758  hashunlem  10783  zfz1isolemiso  10818  seq3coll  10821  shftfvalg  10826  shftfibg  10828  shftfval  10829  shftfib  10831  shftfn  10832  2shfti  10839  shftidt2  10840  caucvgre  10989  cvg1nlemcau  10992  cvg1nlemres  10993  resqrexlemdecn  11020  resqrexlemoverl  11029  resqrexlemglsq  11030  resqrexlemsqa  11032  resqrexlemex  11033  abs00ap  11070  absdiflt  11100  absdifle  11101  lenegsq  11103  cau3lem  11122  minmax  11237  xrmaxltsup  11265  xrminmax  11272  xrltmininf  11277  xrlemininf  11278  clim  11288  clim2  11290  clim0  11292  clim0c  11293  climi0  11296  climuni  11300  2clim  11308  climshftlemg  11309  climshft  11311  climabs0  11314  climcn1  11315  climcn2  11316  addcn2  11317  subcn2  11318  mulcn2  11319  iser3shft  11353  climcau  11354  serf0  11359  sumeq1  11362  sumeq2  11366  sumrbdc  11386  summodclem2  11389  summodc  11390  zsumdc  11391  isumshft  11497  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  prodfap0  11552  prodfrecap  11553  prodfdivap  11554  ntrivcvgap  11555  ntrivcvgap0  11556  prodeq1f  11559  prodeq2w  11563  prodeq2  11564  prodrbdclem2  11580  prodmodclem2  11584  prodmodc  11585  zproddc  11586  fprodntrivap  11591  fprodap0  11628  fprodrec  11636  fproddivapf  11638  fprodap0f  11643  tanaddaplem  11745  sin01bnd  11764  cos01bnd  11765  halfleoddlt  11898  gcddvds  11963  dvdssq  12031  lcmgcdlem  12076  lcmdvds  12078  isprm  12108  prmgt1  12131  isprm5lem  12140  isprm6  12146  pw2dvdslemn  12164  pw2dvdseu  12167  oddpwdclemxy  12168  oddpwdclemndvds  12170  oddpwdclemodd  12171  odzdvds  12244  pclem0  12285  pclemub  12286  pclemdc  12287  pcprecl  12288  pcprendvds  12289  pcpremul  12292  pceulem  12293  pcval  12295  pcelnn  12319  pc2dvds  12328  pcadd  12338  pcmpt  12340  prmpwdvds  12352  imasaddfnlemg  12734  blfvalps  13855  elblps  13860  elbl  13861  elbl3ps  13864  elbl3  13865  blres  13904  comet  13969  bdbl  13973  xmetxp  13977  xmetxpbl  13978  metcnp2  13983  txmetcnp  13988  cnbl0  14004  cnblcld  14005  bl2ioo  14012  addcncntoplem  14021  divcnap  14025  elcncf  14030  elcncf2  14031  cncfi  14035  rescncf  14038  mulc1cncf  14046  cncfco  14048  cncfmet  14049  cncfmptid  14053  addccncf  14056  cdivcncfap  14057  negcncf  14058  mulcncflem  14060  mulcncf  14061  ivthinclemlm  14082  ivthinclemlopn  14084  ivthinclemlr  14085  ivthinclemuopn  14086  ivthinclemur  14087  ivthinclemdisj  14088  ivthinclemloc  14089  ivthinc  14091  limccl  14098  ellimc3apf  14099  limcdifap  14101  limcmpted  14102  limcimolemlt  14103  limcresi  14105  cnplimcim  14106  limccnpcntop  14114  limccnp2lem  14115  limccoap  14117  dvcoapbr  14141  dveflem  14157  eflt  14166  sincosq2sgn  14218  sincosq3sgn  14219  sincosq4sgn  14220  logltb  14265  logge0b  14281  loggt0b  14282  lgslem2  14372  lgslem3  14373  lgsval  14375  lgsfcl2  14377  lgsfle1  14380  lgsle1  14386  lgsdirprm  14405  lgsne0  14409  qdencn  14745  trilpolemlt1  14759