Theorem breq1d 3934

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

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

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 2119

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-v 2683  df-un 3070  df-sn 3528  df-pr 3529  df-op 3531  df-br 3925

This theorem is referenced by:  eqbrtrd  3945  eqbrtrdi  3962  sbcbr2g  3980  pofun  4229  fmptco  5579  isorel  5702  isocnv  5705  isotr  5710  imbrov2fvoveq  5792  caovordig  5929  caovordg  5931  caovord  5935  xporderlem  6121  reldmtpos  6143  brtposg  6144  tpostpos  6154  tposoprab  6170  th3qlem2  6525  ensn1g  6684  fndmeng  6697  xpsneng  6709  xpcomco  6713  snnen2oprc  6747  tridc  6786  fimax2gtrilemstep  6787  unsnfidcel  6802  pm54.43  7039  ccfunen  7072  ltsonq  7199  ltanqg  7201  ltmnqg  7202  archnqq  7218  prloc  7292  addnqprulem  7329  appdivnq  7364  mulnqpru  7370  mullocprlem  7371  1idpru  7392  cauappcvgprlemm  7446  cauappcvgprlemopl  7447  cauappcvgprlemlol  7448  cauappcvgprlemdisj  7452  cauappcvgprlemloc  7453  cauappcvgprlemladdfl  7456  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  cauappcvgprlem1  7460  cauappcvgprlem2  7461  cauappcvgprlemlim  7462  cauappcvgpr  7463  caucvgprlemnkj  7467  caucvgprlemnbj  7468  caucvgprlemm  7469  caucvgprlemopl  7470  caucvgprlemlol  7471  caucvgprlemdisj  7475  caucvgprlemloc  7476  caucvgprlemcl  7477  caucvgprlemladdfu  7478  caucvgprlemladdrl  7479  caucvgprlem1  7480  caucvgprlem2  7481  caucvgpr  7483  caucvgprprlemell  7486  caucvgprprlemelu  7487  caucvgprprlemcbv  7488  caucvgprprlemval  7489  caucvgprprlemnkltj  7490  caucvgprprlemnkeqj  7491  caucvgprprlemnbj  7494  caucvgprprlemml  7495  caucvgprprlemmu  7496  caucvgprprlemopl  7498  caucvgprprlemlol  7499  caucvgprprlemopu  7500  caucvgprprlemloc  7504  caucvgprprlemclphr  7506  caucvgprprlemexbt  7507  caucvgprprlemexb  7508  caucvgprprlemaddq  7509  caucvgprprlem1  7510  caucvgprprlem2  7511  ltsosr  7565  ltasrg  7571  addgt0sr  7576  mulextsr1  7582  prsrlt  7588  caucvgsrlemgt1  7596  caucvgsrlemoffres  7601  caucvgsr  7603  ltpsrprg  7604  pitonnlem2  7648  pitonn  7649  recidpipr  7657  axpre-ltadd  7687  axpre-mulext  7689  nntopi  7695  axcaucvglemval  7698  axcaucvglemcau  7699  axcaucvglemres  7700  ltaddnegr  8180  ltsubadd  8187  lesubadd  8189  ltaddsub2  8192  leaddsub2  8194  ltaddpos  8207  lesub2  8212  ltsub2  8214  ltnegcon2  8219  lenegcon2  8222  addge01  8227  subge0  8230  suble0  8231  lesub0  8234  ltordlem  8237  apreap  8342  divap0b  8436  mulgt1  8614  ltmulgt11  8615  gt0div  8621  ge0div  8622  ltmuldiv  8625  ltmuldiv2  8626  lemuldiv2  8633  ltrec  8634  lerec2  8640  ltdiv23  8643  lediv23  8644  sup3exmid  8708  addltmul  8949  avglt1  8951  avgle1  8953  div4p1lem1div2  8966  ztri3or  9090  zlem1lt  9103  zgt0ge1  9105  qapne  9424  divlt1lt  9504  divle1le  9505  xrltso  9575  xltnegi  9611  xltadd1  9652  xposdif  9658  xlesubadd  9659  xleaddadd  9663  nn0disj  9908  qavgle  10029  frec2uzf1od  10172  iseqf1olemfvp  10263  exp3vallem  10287  expap0  10316  leexp2r  10340  sqap0  10352  nn0opthlem1d  10459  hashennnuni  10518  hashunlem  10543  zfz1isolemiso  10575  seq3coll  10578  shftfvalg  10583  shftfibg  10585  shftfval  10586  shftfib  10588  shftfn  10589  2shfti  10596  shftidt2  10597  caucvgre  10746  cvg1nlemcau  10749  cvg1nlemres  10750  resqrexlemdecn  10777  resqrexlemoverl  10786  resqrexlemglsq  10787  resqrexlemsqa  10789  resqrexlemex  10790  abs00ap  10827  absdiflt  10857  absdifle  10858  lenegsq  10860  cau3lem  10879  minmax  10994  xrmaxltsup  11020  xrminmax  11027  xrltmininf  11032  xrlemininf  11033  clim  11043  clim2  11045  clim0  11047  clim0c  11048  climi0  11051  climuni  11055  2clim  11063  climshftlemg  11064  climshft  11066  climabs0  11069  climcn1  11070  climcn2  11071  addcn2  11072  subcn2  11073  mulcn2  11074  iser3shft  11108  climcau  11109  serf0  11114  sumeq1  11117  sumeq2  11121  sumrbdc  11140  summodclem2  11144  summodc  11145  zsumdc  11146  isumshft  11252  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  prodfap0  11307  prodfrecap  11308  prodfdivap  11309  ntrivcvgap  11310  ntrivcvgap0  11311  prodeq1f  11314  prodeq2w  11318  prodeq2  11319  prodrbdclem2  11335  tanaddaplem  11434  sin01bnd  11453  cos01bnd  11454  halfleoddlt  11580  gcddvds  11641  dvdssq  11708  lcmgcdlem  11747  lcmdvds  11749  isprm  11779  prmgt1  11801  isprm6  11814  pw2dvdslemn  11832  pw2dvdseu  11835  oddpwdclemxy  11836  oddpwdclemndvds  11838  oddpwdclemodd  11839  blfvalps  12543  elblps  12548  elbl  12549  elbl3ps  12552  elbl3  12553  blres  12592  comet  12657  bdbl  12661  xmetxp  12665  xmetxpbl  12666  metcnp2  12671  txmetcnp  12676  cnbl0  12692  cnblcld  12693  bl2ioo  12700  addcncntoplem  12709  divcnap  12713  elcncf  12718  elcncf2  12719  cncfi  12723  rescncf  12726  mulc1cncf  12734  cncfco  12736  cncfmet  12737  cncfmptid  12741  addccncf  12744  cdivcncfap  12745  negcncf  12746  mulcncflem  12748  mulcncf  12749  ivthinclemlm  12770  ivthinclemlopn  12772  ivthinclemlr  12773  ivthinclemuopn  12774  ivthinclemur  12775  ivthinclemdisj  12776  ivthinclemloc  12777  ivthinc  12779  limccl  12786  ellimc3apf  12787  limcdifap  12789  limcmpted  12790  limcimolemlt  12791  limcresi  12793  cnplimcim  12794  limccnpcntop  12802  limccnp2lem  12803  limccoap  12805  dvcoapbr  12829  dveflem  12844  sincosq2sgn  12897  sincosq3sgn  12898  sincosq4sgn  12899  qdencn  13211  trilpolemlt1  13223