Theorem breq1d 4092

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   class class class wbr 4082

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4083

This theorem is referenced by:  eqnbrtrd  4100  eqbrtrd  4104  eqbrtrdi  4121  sbcbr2g  4140  pofun  4402  fmptco  5800  isorel  5931  isocnv  5934  isotr  5939  imbrov2fvoveq  6025  caovordig  6170  caovordg  6172  caovord  6176  xporderlem  6375  reldmtpos  6397  brtposg  6398  tpostpos  6408  tposoprab  6424  th3qlem2  6783  ensn1g  6947  fndmeng  6961  xpsneng  6977  xpcomco  6981  snnen2oprc  7017  tridc  7057  fimax2gtrilemstep  7058  unsnfidcel  7079  pm54.43  7359  pr1or2  7363  ccfunen  7446  ltsonq  7581  ltanqg  7583  ltmnqg  7584  archnqq  7600  prloc  7674  addnqprulem  7711  appdivnq  7746  mulnqpru  7752  mullocprlem  7753  1idpru  7774  cauappcvgprlemm  7828  cauappcvgprlemopl  7829  cauappcvgprlemlol  7830  cauappcvgprlemdisj  7834  cauappcvgprlemloc  7835  cauappcvgprlemladdfl  7838  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  cauappcvgprlem1  7842  cauappcvgprlem2  7843  cauappcvgprlemlim  7844  cauappcvgpr  7845  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemm  7851  caucvgprlemopl  7852  caucvgprlemlol  7853  caucvgprlemdisj  7857  caucvgprlemloc  7858  caucvgprlemcl  7859  caucvgprlemladdfu  7860  caucvgprlemladdrl  7861  caucvgprlem1  7862  caucvgprlem2  7863  caucvgpr  7865  caucvgprprlemell  7868  caucvgprprlemelu  7869  caucvgprprlemcbv  7870  caucvgprprlemval  7871  caucvgprprlemnkltj  7872  caucvgprprlemnkeqj  7873  caucvgprprlemnbj  7876  caucvgprprlemml  7877  caucvgprprlemmu  7878  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemopu  7882  caucvgprprlemloc  7886  caucvgprprlemclphr  7888  caucvgprprlemexbt  7889  caucvgprprlemexb  7890  caucvgprprlemaddq  7891  caucvgprprlem1  7892  caucvgprprlem2  7893  ltsosr  7947  ltasrg  7953  addgt0sr  7958  mulextsr1  7964  prsrlt  7970  caucvgsrlemgt1  7978  caucvgsrlemoffres  7983  caucvgsr  7985  ltpsrprg  7986  pitonnlem2  8030  pitonn  8031  recidpipr  8039  axpre-ltadd  8069  axpre-mulext  8071  nntopi  8077  axcaucvglemval  8080  axcaucvglemcau  8081  axcaucvglemres  8082  ltaddnegr  8568  ltsubadd  8575  lesubadd  8577  ltaddsub2  8580  leaddsub2  8582  ltaddpos  8595  lesub2  8600  ltsub2  8602  ltnegcon2  8607  lenegcon2  8610  addge01  8615  subge0  8618  suble0  8619  lesub0  8622  ltordlem  8625  apreap  8730  divap0b  8826  mulgt1  9006  ltmulgt11  9007  gt0div  9013  ge0div  9014  ltmuldiv  9017  ltmuldiv2  9018  lemuldiv2  9025  ltrec  9026  lerec2  9032  ltdiv23  9035  lediv23  9036  sup3exmid  9100  addltmul  9344  avglt1  9346  avgle1  9348  div4p1lem1div2  9361  ztri3or  9485  zlem1lt  9499  zgt0ge1  9501  qapne  9830  irrmulap  9839  divlt1lt  9916  divle1le  9917  xrltso  9988  xltnegi  10027  xltadd1  10068  xposdif  10074  xlesubadd  10075  xleaddadd  10079  nn0disj  10330  qavgle  10473  fldiv4lem1div2uz2  10521  frec2uzf1od  10623  iseqf1olemfvp  10727  seqf1oglem1  10736  exp3vallem  10757  expap0  10786  leexp2r  10810  sqap0  10823  nn0ltexp2  10926  nn0opthlem1d  10937  hashennnuni  10996  hashunlem  11021  zfz1isolemiso  11056  seq3coll  11059  swrdccatin2  11256  shftfvalg  11324  shftfibg  11326  shftfval  11327  shftfib  11329  shftfn  11330  2shfti  11337  shftidt2  11338  caucvgre  11487  cvg1nlemcau  11490  cvg1nlemres  11491  resqrexlemdecn  11518  resqrexlemoverl  11527  resqrexlemglsq  11528  resqrexlemsqa  11530  resqrexlemex  11531  abs00ap  11568  absdiflt  11598  absdifle  11599  lenegsq  11601  cau3lem  11620  minmax  11736  xrmaxltsup  11764  xrminmax  11771  xrltmininf  11776  xrlemininf  11777  clim  11787  clim2  11789  clim0  11791  clim0c  11792  climi0  11795  climuni  11799  2clim  11807  climshftlemg  11808  climshft  11810  climabs0  11813  climcn1  11814  climcn2  11815  addcn2  11816  subcn2  11817  mulcn2  11818  iser3shft  11852  climcau  11853  serf0  11858  sumeq1  11861  sumeq2  11865  sumrbdc  11885  summodclem2  11888  summodc  11889  zsumdc  11890  isumshft  11996  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  prodfap0  12051  prodfrecap  12052  prodfdivap  12053  ntrivcvgap  12054  ntrivcvgap0  12055  prodeq1f  12058  prodeq2w  12062  prodeq2  12063  prodrbdclem2  12079  prodmodclem2  12083  prodmodc  12084  zproddc  12085  fprodntrivap  12090  fprodap0  12127  fprodrec  12135  fproddivapf  12137  fprodap0f  12142  tanaddaplem  12244  sin01bnd  12263  cos01bnd  12264  halfleoddlt  12400  gcddvds  12479  dvdssq  12547  lcmgcdlem  12594  lcmdvds  12596  isprm  12626  prmgt1  12649  isprm5lem  12658  isprm6  12664  pw2dvdslemn  12682  pw2dvdseu  12685  oddpwdclemxy  12686  oddpwdclemndvds  12688  oddpwdclemodd  12689  odzdvds  12763  pclem0  12804  pclemub  12805  pclemdc  12806  pcprecl  12807  pcprendvds  12808  pcpremul  12811  pceulem  12812  pcval  12814  pcelnn  12839  pc2dvds  12848  pcadd  12858  pcadd2  12859  pcmpt  12861  prmpwdvds  12873  4sqlem17  12925  imasaddfnlemg  13342  znf1o  14609  znidomb  14616  mplsubgfilemm  14656  mplsubgfilemcl  14657  blfvalps  15053  elblps  15058  elbl  15059  elbl3ps  15062  elbl3  15063  blres  15102  comet  15167  bdbl  15171  xmetxp  15175  xmetxpbl  15176  metcnp2  15181  txmetcnp  15186  cnbl0  15202  cnblcld  15203  bl2ioo  15218  addcncntoplem  15229  divcnap  15233  mpomulcn  15234  elcncf  15241  elcncf2  15242  cncfi  15246  rescncf  15249  mulc1cncf  15257  cncfco  15259  cncfmet  15260  cncfmptid  15265  addccncf  15268  cdivcncfap  15272  negcncf  15273  mulcncflem  15275  mulcncf  15276  ivthinclemlm  15302  ivthinclemlopn  15304  ivthinclemlr  15305  ivthinclemuopn  15306  ivthinclemur  15307  ivthinclemdisj  15308  ivthinclemloc  15309  ivthinc  15311  ivthreinc  15313  limccl  15327  ellimc3apf  15328  limcdifap  15330  limcmpted  15331  limcimolemlt  15332  limcresi  15334  cnplimcim  15335  limccnpcntop  15343  limccnp2lem  15344  limccoap  15346  dvcoapbr  15375  dveflem  15394  eflt  15443  sincosq2sgn  15495  sincosq3sgn  15496  sincosq4sgn  15497  logltb  15542  logge0b  15558  loggt0b  15559  lgslem2  15674  lgslem3  15675  lgsval  15677  lgsfcl2  15679  lgsfle1  15682  lgsle1  15688  lgsdirprm  15707  lgsne0  15711  gausslemma2dlem1a  15731  gausslemma2dlem1f1o  15733  gausslemma2dlem2  15735  gausslemma2dlem3  15736  gausslemma2dlem4  15737  qdencn  16354  trilpolemlt1  16368