Theorem breq1d 4135

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402   class class class wbr 4125

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-br 4126

This theorem is referenced by:  eqnbrtrd  4143  eqbrtrd  4147  eqbrtrdi  4164  sbcbr2g  4183  pofun  4452  fmptco  5865  isorel  6004  isocnv  6007  isotr  6012  imbrov2fvoveq  6100  caovordig  6245  caovordg  6247  caovord  6251  xporderlem  6457  reldmtpos  6514  brtposg  6515  tpostpos  6525  tposoprab  6541  th3qlem2  6902  ensn1g  7074  fndmeng  7088  xpsneng  7110  xpcomco  7114  snnen2oprc  7151  tridc  7194  fimax2gtrilemstep  7195  unsnfidcel  7218  pm54.43  7526  pr1or2  7530  ccfunen  7620  ltsonq  7755  ltanqg  7757  ltmnqg  7758  archnqq  7774  prloc  7848  addnqprulem  7885  appdivnq  7920  mulnqpru  7926  mullocprlem  7927  1idpru  7948  cauappcvgprlemm  8002  cauappcvgprlemopl  8003  cauappcvgprlemlol  8004  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlemladdfl  8012  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem1  8016  cauappcvgprlem2  8017  cauappcvgprlemlim  8018  cauappcvgpr  8019  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemlol  8027  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprlemcl  8033  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  caucvgprlem1  8036  caucvgprlem2  8037  caucvgpr  8039  caucvgprprlemell  8042  caucvgprprlemelu  8043  caucvgprprlemcbv  8044  caucvgprprlemval  8045  caucvgprprlemnkltj  8046  caucvgprprlemnkeqj  8047  caucvgprprlemnbj  8050  caucvgprprlemml  8051  caucvgprprlemmu  8052  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemopu  8056  caucvgprprlemloc  8060  caucvgprprlemclphr  8062  caucvgprprlemexbt  8063  caucvgprprlemexb  8064  caucvgprprlemaddq  8065  caucvgprprlem1  8066  caucvgprprlem2  8067  ltsosr  8121  ltasrg  8127  addgt0sr  8132  mulextsr1  8138  prsrlt  8144  caucvgsrlemgt1  8152  caucvgsrlemoffres  8157  caucvgsr  8159  ltpsrprg  8160  pitonnlem2  8204  pitonn  8205  recidpipr  8213  axpre-ltadd  8243  axpre-mulext  8245  nntopi  8251  axcaucvglemval  8254  axcaucvglemcau  8255  axcaucvglemres  8256  ltaddnegr  8743  ltsubadd  8750  lesubadd  8752  ltaddsub2  8755  leaddsub2  8757  ltaddpos  8770  lesub2  8775  ltsub2  8777  ltnegcon2  8782  lenegcon2  8785  addge01  8790  subge0  8793  suble0  8794  lesub0  8797  ltordlem  8800  apreap  8905  divap0b  9003  mulgt1  9183  ltmulgt11  9184  gt0div  9190  ge0div  9191  ltmuldiv  9194  ltmuldiv2  9195  lemuldiv2  9202  ltrec  9203  lerec2  9209  ltdiv23  9212  lediv23  9213  sup3exmid  9277  addltmul  9521  avglt1  9523  avgle1  9525  div4p1lem1div2  9538  ztri3or  9666  zlem1lt  9680  zgt0ge1  9682  qapne  10018  irrmulap  10027  divlt1lt  10104  divle1le  10105  xrltso  10177  xltnegi  10216  xltadd1  10257  xposdif  10263  xlesubadd  10264  xleaddadd  10268  nn0disj  10523  qavgle  10671  fldiv4lem1div2uz2  10719  frec2uzf1od  10821  iseqf1olemfvp  10925  seqf1oglem1  10934  exp3vallem  10955  expap0  10984  leexp2r  11008  sqap0  11021  nn0ltexp2  11125  nn0opthlem1d  11136  hashennnuni  11196  hashunlem  11222  hashf1  11265  zfz1isolemiso  11269  seq3coll  11272  swrdccatin2  11479  shftfvalg  11561  shftfibg  11563  shftfval  11564  shftfib  11566  shftfn  11567  2shfti  11574  shftidt2  11575  caucvgre  11725  cvg1nlemcau  11728  cvg1nlemres  11729  resqrexlemdecn  11756  resqrexlemoverl  11765  resqrexlemglsq  11766  resqrexlemsqa  11768  resqrexlemex  11769  abs00ap  11806  absdiflt  11836  absdifle  11837  lenegsq  11839  cau3lem  11858  minmax  11974  xrmaxltsup  12002  xrminmax  12009  xrltmininf  12014  xrlemininf  12015  clim  12025  clim2  12027  clim0  12029  clim0c  12030  climi0  12033  climuni  12037  2clim  12045  climshftlemg  12046  climshft  12048  climabs0  12051  climcn1  12052  climcn2  12053  addcn2  12054  subcn2  12055  mulcn2  12056  iser3shft  12090  climcau  12091  serf0  12096  sumeq1  12099  sumeq2  12103  sumrbdc  12124  summodclem2  12127  summodc  12128  zsumdc  12129  isumshft  12235  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  prodfap0  12290  prodfrecap  12291  prodfdivap  12292  ntrivcvgap  12293  ntrivcvgap0  12294  prodeq1f  12297  prodeq2w  12301  prodeq2  12302  prodrbdclem2  12318  prodmodclem2  12322  prodmodc  12323  zproddc  12324  fprodntrivap  12329  fprodap0  12366  fprodrec  12374  fproddivapf  12376  fprodap0f  12381  tanaddaplem  12483  sin01bnd  12502  cos01bnd  12503  halfleoddlt  12639  gcddvds  12718  dvdssq  12786  lcmgcdlem  12833  lcmdvds  12835  isprm  12865  prmgt1  12888  isprm5lem  12897  isprm6  12903  pw2dvdslemn  12921  pw2dvdseu  12924  oddpwdclemxy  12925  oddpwdclemndvds  12927  oddpwdclemodd  12928  odzdvds  13002  pclem0  13043  pclemub  13044  pclemdc  13045  pcprecl  13046  pcprendvds  13047  pcpremul  13050  pceulem  13051  pcval  13053  pcelnn  13078  pc2dvds  13087  pcadd  13097  pcadd2  13098  pcmpt  13100  prmpwdvds  13112  4sqlem17  13164  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemodife  13218  ballotfilemic  13228  ballotfilemsv  13231  ballotfilemrc  13252  imasaddfnlemg  13612  znf1o  14958  znidomb  14965  mplsubgfilemm  15012  mplsubgfilemcl  15013  blfvalps  15409  elblps  15414  elbl  15415  elbl3ps  15418  elbl3  15419  blres  15458  comet  15523  bdbl  15527  xmetxp  15531  xmetxpbl  15532  metcnp2  15537  txmetcnp  15542  cnbl0  15558  cnblcld  15559  bl2ioo  15574  addcncntoplem  15585  divcnap  15589  mpomulcn  15590  elcncf  15597  elcncf2  15598  cncfi  15602  rescncf  15605  mulc1cncf  15613  cncfco  15615  cncfmet  15616  cncfmptid  15621  addccncf  15624  cdivcncfap  15628  negcncf  15629  mulcncflem  15631  mulcncf  15632  ivthinclemlm  15658  ivthinclemlopn  15660  ivthinclemlr  15661  ivthinclemuopn  15662  ivthinclemur  15663  ivthinclemdisj  15664  ivthinclemloc  15665  ivthinc  15667  ivthreinc  15669  limccl  15683  ellimc3apf  15684  limcdifap  15686  limcmpted  15687  limcimolemlt  15688  limcresi  15690  cnplimcim  15691  limccnpcntop  15699  limccnp2lem  15700  limccoap  15702  dvcoapbr  15731  dveflem  15750  eflt  15799  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  logltb  15898  logge0b  15914  loggt0b  15915  pellexlem3  16007  lgslem2  16034  lgslem3  16035  lgsval  16037  lgsfcl2  16039  lgsfle1  16042  lgsle1  16048  lgsdirprm  16067  lgsne0  16071  gausslemma2dlem1a  16091  gausslemma2dlem1f1o  16093  gausslemma2dlem2  16095  gausslemma2dlem3  16096  gausslemma2dlem4  16097  subupgr  16428  vtxdumgrfival  16453  qdencn  16977  trilpolemlt1  16995