Theorem breq1d 3939

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1331   class class class wbr 3929

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930

This theorem is referenced by:  eqbrtrd  3950  eqbrtrdi  3967  sbcbr2g  3985  pofun  4234  fmptco  5586  isorel  5709  isocnv  5712  isotr  5717  imbrov2fvoveq  5799  caovordig  5936  caovordg  5938  caovord  5942  xporderlem  6128  reldmtpos  6150  brtposg  6151  tpostpos  6161  tposoprab  6177  th3qlem2  6532  ensn1g  6691  fndmeng  6704  xpsneng  6716  xpcomco  6720  snnen2oprc  6754  tridc  6793  fimax2gtrilemstep  6794  unsnfidcel  6809  pm54.43  7046  ccfunen  7079  ltsonq  7213  ltanqg  7215  ltmnqg  7216  archnqq  7232  prloc  7306  addnqprulem  7343  appdivnq  7378  mulnqpru  7384  mullocprlem  7385  1idpru  7406  cauappcvgprlemm  7460  cauappcvgprlemopl  7461  cauappcvgprlemlol  7462  cauappcvgprlemdisj  7466  cauappcvgprlemloc  7467  cauappcvgprlemladdfl  7470  cauappcvgprlemladdru  7471  cauappcvgprlemladdrl  7472  cauappcvgprlem1  7474  cauappcvgprlem2  7475  cauappcvgprlemlim  7476  cauappcvgpr  7477  caucvgprlemnkj  7481  caucvgprlemnbj  7482  caucvgprlemm  7483  caucvgprlemopl  7484  caucvgprlemlol  7485  caucvgprlemdisj  7489  caucvgprlemloc  7490  caucvgprlemcl  7491  caucvgprlemladdfu  7492  caucvgprlemladdrl  7493  caucvgprlem1  7494  caucvgprlem2  7495  caucvgpr  7497  caucvgprprlemell  7500  caucvgprprlemelu  7501  caucvgprprlemcbv  7502  caucvgprprlemval  7503  caucvgprprlemnkltj  7504  caucvgprprlemnkeqj  7505  caucvgprprlemnbj  7508  caucvgprprlemml  7509  caucvgprprlemmu  7510  caucvgprprlemopl  7512  caucvgprprlemlol  7513  caucvgprprlemopu  7514  caucvgprprlemloc  7518  caucvgprprlemclphr  7520  caucvgprprlemexbt  7521  caucvgprprlemexb  7522  caucvgprprlemaddq  7523  caucvgprprlem1  7524  caucvgprprlem2  7525  ltsosr  7579  ltasrg  7585  addgt0sr  7590  mulextsr1  7596  prsrlt  7602  caucvgsrlemgt1  7610  caucvgsrlemoffres  7615  caucvgsr  7617  ltpsrprg  7618  pitonnlem2  7662  pitonn  7663  recidpipr  7671  axpre-ltadd  7701  axpre-mulext  7703  nntopi  7709  axcaucvglemval  7712  axcaucvglemcau  7713  axcaucvglemres  7714  ltaddnegr  8194  ltsubadd  8201  lesubadd  8203  ltaddsub2  8206  leaddsub2  8208  ltaddpos  8221  lesub2  8226  ltsub2  8228  ltnegcon2  8233  lenegcon2  8236  addge01  8241  subge0  8244  suble0  8245  lesub0  8248  ltordlem  8251  apreap  8356  divap0b  8450  mulgt1  8628  ltmulgt11  8629  gt0div  8635  ge0div  8636  ltmuldiv  8639  ltmuldiv2  8640  lemuldiv2  8647  ltrec  8648  lerec2  8654  ltdiv23  8657  lediv23  8658  sup3exmid  8722  addltmul  8963  avglt1  8965  avgle1  8967  div4p1lem1div2  8980  ztri3or  9104  zlem1lt  9117  zgt0ge1  9119  qapne  9438  divlt1lt  9518  divle1le  9519  xrltso  9589  xltnegi  9625  xltadd1  9666  xposdif  9672  xlesubadd  9673  xleaddadd  9677  nn0disj  9922  qavgle  10043  frec2uzf1od  10186  iseqf1olemfvp  10277  exp3vallem  10301  expap0  10330  leexp2r  10354  sqap0  10366  nn0opthlem1d  10473  hashennnuni  10532  hashunlem  10557  zfz1isolemiso  10589  seq3coll  10592  shftfvalg  10597  shftfibg  10599  shftfval  10600  shftfib  10602  shftfn  10603  2shfti  10610  shftidt2  10611  caucvgre  10760  cvg1nlemcau  10763  cvg1nlemres  10764  resqrexlemdecn  10791  resqrexlemoverl  10800  resqrexlemglsq  10801  resqrexlemsqa  10803  resqrexlemex  10804  abs00ap  10841  absdiflt  10871  absdifle  10872  lenegsq  10874  cau3lem  10893  minmax  11008  xrmaxltsup  11034  xrminmax  11041  xrltmininf  11046  xrlemininf  11047  clim  11057  clim2  11059  clim0  11061  clim0c  11062  climi0  11065  climuni  11069  2clim  11077  climshftlemg  11078  climshft  11080  climabs0  11083  climcn1  11084  climcn2  11085  addcn2  11086  subcn2  11087  mulcn2  11088  iser3shft  11122  climcau  11123  serf0  11128  sumeq1  11131  sumeq2  11135  sumrbdc  11155  summodclem2  11158  summodc  11159  zsumdc  11160  isumshft  11266  mertenslemi1  11311  mertenslem2  11312  mertensabs  11313  prodfap0  11321  prodfrecap  11322  prodfdivap  11323  ntrivcvgap  11324  ntrivcvgap0  11325  prodeq1f  11328  prodeq2w  11332  prodeq2  11333  prodrbdclem2  11349  prodmodclem2  11353  prodmodc  11354  tanaddaplem  11452  sin01bnd  11471  cos01bnd  11472  halfleoddlt  11598  gcddvds  11659  dvdssq  11726  lcmgcdlem  11765  lcmdvds  11767  isprm  11797  prmgt1  11819  isprm6  11832  pw2dvdslemn  11850  pw2dvdseu  11853  oddpwdclemxy  11854  oddpwdclemndvds  11856  oddpwdclemodd  11857  blfvalps  12564  elblps  12569  elbl  12570  elbl3ps  12573  elbl3  12574  blres  12613  comet  12678  bdbl  12682  xmetxp  12686  xmetxpbl  12687  metcnp2  12692  txmetcnp  12697  cnbl0  12713  cnblcld  12714  bl2ioo  12721  addcncntoplem  12730  divcnap  12734  elcncf  12739  elcncf2  12740  cncfi  12744  rescncf  12747  mulc1cncf  12755  cncfco  12757  cncfmet  12758  cncfmptid  12762  addccncf  12765  cdivcncfap  12766  negcncf  12767  mulcncflem  12769  mulcncf  12770  ivthinclemlm  12791  ivthinclemlopn  12793  ivthinclemlr  12794  ivthinclemuopn  12795  ivthinclemur  12796  ivthinclemdisj  12797  ivthinclemloc  12798  ivthinc  12800  limccl  12807  ellimc3apf  12808  limcdifap  12810  limcmpted  12811  limcimolemlt  12812  limcresi  12814  cnplimcim  12815  limccnpcntop  12823  limccnp2lem  12824  limccoap  12826  dvcoapbr  12850  dveflem  12865  sincosq2sgn  12918  sincosq3sgn  12919  sincosq4sgn  12920  qdencn  13232  trilpolemlt1  13244