Theorem breq1d 4039

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030

This theorem is referenced by:  eqnbrtrd  4047  eqbrtrd  4051  eqbrtrdi  4068  sbcbr2g  4086  pofun  4343  fmptco  5724  isorel  5851  isocnv  5854  isotr  5859  imbrov2fvoveq  5943  caovordig  6084  caovordg  6086  caovord  6090  xporderlem  6284  reldmtpos  6306  brtposg  6307  tpostpos  6317  tposoprab  6333  th3qlem2  6692  ensn1g  6851  fndmeng  6864  xpsneng  6876  xpcomco  6880  snnen2oprc  6916  tridc  6955  fimax2gtrilemstep  6956  unsnfidcel  6977  pm54.43  7250  ccfunen  7324  ltsonq  7458  ltanqg  7460  ltmnqg  7461  archnqq  7477  prloc  7551  addnqprulem  7588  appdivnq  7623  mulnqpru  7629  mullocprlem  7630  1idpru  7651  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlemladdfl  7715  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem1  7719  cauappcvgprlem2  7720  cauappcvgprlemlim  7721  cauappcvgpr  7722  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemcl  7736  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  caucvgprlem1  7739  caucvgprlem2  7740  caucvgpr  7742  caucvgprprlemell  7745  caucvgprprlemelu  7746  caucvgprprlemcbv  7747  caucvgprprlemval  7748  caucvgprprlemnkltj  7749  caucvgprprlemnkeqj  7750  caucvgprprlemnbj  7753  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemopu  7759  caucvgprprlemloc  7763  caucvgprprlemclphr  7765  caucvgprprlemexbt  7766  caucvgprprlemexb  7767  caucvgprprlemaddq  7768  caucvgprprlem1  7769  caucvgprprlem2  7770  ltsosr  7824  ltasrg  7830  addgt0sr  7835  mulextsr1  7841  prsrlt  7847  caucvgsrlemgt1  7855  caucvgsrlemoffres  7860  caucvgsr  7862  ltpsrprg  7863  pitonnlem2  7907  pitonn  7908  recidpipr  7916  axpre-ltadd  7946  axpre-mulext  7948  nntopi  7954  axcaucvglemval  7957  axcaucvglemcau  7958  axcaucvglemres  7959  ltaddnegr  8444  ltsubadd  8451  lesubadd  8453  ltaddsub2  8456  leaddsub2  8458  ltaddpos  8471  lesub2  8476  ltsub2  8478  ltnegcon2  8483  lenegcon2  8486  addge01  8491  subge0  8494  suble0  8495  lesub0  8498  ltordlem  8501  apreap  8606  divap0b  8702  mulgt1  8882  ltmulgt11  8883  gt0div  8889  ge0div  8890  ltmuldiv  8893  ltmuldiv2  8894  lemuldiv2  8901  ltrec  8902  lerec2  8908  ltdiv23  8911  lediv23  8912  sup3exmid  8976  addltmul  9219  avglt1  9221  avgle1  9223  div4p1lem1div2  9236  ztri3or  9360  zlem1lt  9373  zgt0ge1  9375  qapne  9704  irrmulap  9713  divlt1lt  9790  divle1le  9791  xrltso  9862  xltnegi  9901  xltadd1  9942  xposdif  9948  xlesubadd  9949  xleaddadd  9953  nn0disj  10204  qavgle  10327  fldiv4lem1div2uz2  10375  frec2uzf1od  10477  iseqf1olemfvp  10581  seqf1oglem1  10590  exp3vallem  10611  expap0  10640  leexp2r  10664  sqap0  10677  nn0ltexp2  10780  nn0opthlem1d  10791  hashennnuni  10850  hashunlem  10875  zfz1isolemiso  10910  seq3coll  10913  shftfvalg  10962  shftfibg  10964  shftfval  10965  shftfib  10967  shftfn  10968  2shfti  10975  shftidt2  10976  caucvgre  11125  cvg1nlemcau  11128  cvg1nlemres  11129  resqrexlemdecn  11156  resqrexlemoverl  11165  resqrexlemglsq  11166  resqrexlemsqa  11168  resqrexlemex  11169  abs00ap  11206  absdiflt  11236  absdifle  11237  lenegsq  11239  cau3lem  11258  minmax  11373  xrmaxltsup  11401  xrminmax  11408  xrltmininf  11413  xrlemininf  11414  clim  11424  clim2  11426  clim0  11428  clim0c  11429  climi0  11432  climuni  11436  2clim  11444  climshftlemg  11445  climshft  11447  climabs0  11450  climcn1  11451  climcn2  11452  addcn2  11453  subcn2  11454  mulcn2  11455  iser3shft  11489  climcau  11490  serf0  11495  sumeq1  11498  sumeq2  11502  sumrbdc  11522  summodclem2  11525  summodc  11526  zsumdc  11527  isumshft  11633  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  prodfap0  11688  prodfrecap  11689  prodfdivap  11690  ntrivcvgap  11691  ntrivcvgap0  11692  prodeq1f  11695  prodeq2w  11699  prodeq2  11700  prodrbdclem2  11716  prodmodclem2  11720  prodmodc  11721  zproddc  11722  fprodntrivap  11727  fprodap0  11764  fprodrec  11772  fproddivapf  11774  fprodap0f  11779  tanaddaplem  11881  sin01bnd  11900  cos01bnd  11901  halfleoddlt  12035  gcddvds  12100  dvdssq  12168  lcmgcdlem  12215  lcmdvds  12217  isprm  12247  prmgt1  12270  isprm5lem  12279  isprm6  12285  pw2dvdslemn  12303  pw2dvdseu  12306  oddpwdclemxy  12307  oddpwdclemndvds  12309  oddpwdclemodd  12310  odzdvds  12383  pclem0  12424  pclemub  12425  pclemdc  12426  pcprecl  12427  pcprendvds  12428  pcpremul  12431  pceulem  12432  pcval  12434  pcelnn  12459  pc2dvds  12468  pcadd  12478  pcadd2  12479  pcmpt  12481  prmpwdvds  12493  4sqlem17  12545  imasaddfnlemg  12897  znf1o  14139  znidomb  14146  blfvalps  14553  elblps  14558  elbl  14559  elbl3ps  14562  elbl3  14563  blres  14602  comet  14667  bdbl  14671  xmetxp  14675  xmetxpbl  14676  metcnp2  14681  txmetcnp  14686  cnbl0  14702  cnblcld  14703  bl2ioo  14710  addcncntoplem  14719  divcnap  14723  elcncf  14728  elcncf2  14729  cncfi  14733  rescncf  14736  mulc1cncf  14744  cncfco  14746  cncfmet  14747  cncfmptid  14751  addccncf  14754  cdivcncfap  14758  negcncf  14759  mulcncflem  14761  mulcncf  14762  ivthinclemlm  14788  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemdisj  14794  ivthinclemloc  14795  ivthinc  14797  ivthreinc  14799  limccl  14813  ellimc3apf  14814  limcdifap  14816  limcmpted  14817  limcimolemlt  14818  limcresi  14820  cnplimcim  14821  limccnpcntop  14829  limccnp2lem  14830  limccoap  14832  dvcoapbr  14856  dveflem  14872  eflt  14910  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  logltb  15009  logge0b  15025  loggt0b  15026  lgslem2  15117  lgslem3  15118  lgsval  15120  lgsfcl2  15122  lgsfle1  15125  lgsle1  15131  lgsdirprm  15150  lgsne0  15154  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  gausslemma2dlem2  15178  gausslemma2dlem3  15179  gausslemma2dlem4  15180  qdencn  15517  trilpolemlt1  15531