Theorem breq1d 4140

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   class class class wbr 4130

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  eqnbrtrd  4148  eqbrtrd  4152  eqbrtrdi  4169  sbcbr2g  4188  pofun  4457  fmptco  5874  isorel  6014  isocnv  6017  isotr  6022  imbrov2fvoveq  6110  caovordig  6255  caovordg  6257  caovord  6261  xporderlem  6467  reldmtpos  6524  brtposg  6525  tpostpos  6535  tposoprab  6551  th3qlem2  6912  ensn1g  7084  fndmeng  7098  xpsneng  7120  xpcomco  7124  snnen2oprc  7161  tridc  7204  fimax2gtrilemstep  7205  unsnfidcel  7228  pm54.43  7536  pr1or2  7540  ccfunen  7630  ltsonq  7765  ltanqg  7767  ltmnqg  7768  archnqq  7784  prloc  7858  addnqprulem  7895  appdivnq  7930  mulnqpru  7936  mullocprlem  7937  1idpru  7958  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlem2  8027  cauappcvgprlemlim  8028  cauappcvgpr  8029  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgprlem2  8047  caucvgpr  8049  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemnbj  8060  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlemclphr  8072  caucvgprprlemexbt  8073  caucvgprprlemexb  8074  caucvgprprlemaddq  8075  caucvgprprlem1  8076  caucvgprprlem2  8077  ltsosr  8131  ltasrg  8137  addgt0sr  8142  mulextsr1  8148  prsrlt  8154  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  caucvgsr  8169  ltpsrprg  8170  pitonnlem2  8214  pitonn  8215  recidpipr  8223  axpre-ltadd  8253  axpre-mulext  8255  nntopi  8261  axcaucvglemval  8264  axcaucvglemcau  8265  axcaucvglemres  8266  ltaddnegr  8754  ltsubadd  8761  lesubadd  8763  ltaddsub2  8766  leaddsub2  8768  ltaddpos  8781  lesub2  8786  ltsub2  8788  ltnegcon2  8793  lenegcon2  8796  addge01  8801  subge0  8804  suble0  8805  lesub0  8808  ltordlem  8811  apreap  8917  divap0b  9015  mulgt1  9195  ltmulgt11  9196  gt0div  9202  ge0div  9203  ltmuldiv  9206  ltmuldiv2  9207  lemuldiv2  9214  ltrec  9215  lerec2  9221  ltdiv23  9224  lediv23  9225  sup3exmid  9289  addltmul  9546  avglt1  9548  avgle1  9550  div4p1lem1div2  9563  ztri3or  9691  zlem1lt  9705  zgt0ge1  9707  qapne  10048  irrmulap  10058  divlt1lt  10135  divle1le  10136  xrltso  10208  xltnegi  10247  xltadd1  10288  xposdif  10294  xlesubadd  10295  xleaddadd  10299  nn0disj  10555  qavgle  10703  fldiv4lem1div2uz2  10754  frec2uzf1od  10856  iseqf1olemfvp  10960  seqf1oglem1  10969  exp3vallem  10990  expap0  11019  leexp2r  11043  sqap0  11056  nn0ltexp2  11161  nn0opthlem1d  11172  hashennnuni  11232  hashunlem  11258  hashf1  11301  zfz1isolemiso  11305  seq3coll  11308  swrdccatin2  11515  shftfvalg  11597  shftfibg  11599  shftfval  11600  shftfib  11602  shftfn  11603  2shfti  11610  shftidt2  11611  caucvgre  11761  cvg1nlemcau  11764  cvg1nlemres  11765  resqrexlemdecn  11792  resqrexlemoverl  11801  resqrexlemglsq  11802  resqrexlemsqa  11804  resqrexlemex  11805  abs00ap  11842  absdiflt  11873  absdifle  11874  lenegsq  11876  cau3lem  11895  minmax  12011  xrmaxltsup  12040  xrminmax  12047  xrltmininf  12052  xrlemininf  12053  clim  12063  clim2  12065  clim0  12067  clim0c  12068  climi0  12071  climuni  12075  2clim  12083  climshftlemg  12084  climshft  12086  climabs0  12089  climcn1  12090  climcn2  12091  addcn2  12092  subcn2  12093  mulcn2  12094  iser3shft  12128  climcau  12129  serf0  12134  sumeq1  12137  sumeq2  12141  sumrbdc  12162  summodclem2  12165  summodc  12166  zsumdc  12167  isumshft  12273  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  prodfap0  12328  prodfrecap  12329  prodfdivap  12330  ntrivcvgap  12331  ntrivcvgap0  12332  prodeq1f  12335  prodeq2w  12339  prodeq2  12340  prodrbdclem2  12356  prodmodclem2  12360  prodmodc  12361  zproddc  12362  fprodntrivap  12367  fprodap0  12404  fprodrec  12412  fproddivapf  12414  fprodap0f  12419  tanaddaplem  12521  sin01bnd  12540  cos01bnd  12541  halfleoddlt  12677  gcddvds  12756  dvdssq  12824  lcmgcdlem  12871  lcmdvds  12873  isprm  12903  prmgt1  12927  isprm5lem  12936  isprm6  12942  pwbdvdslemn  12960  pwbdvdseu  12963  nnmaxpwlemxy  12964  nnmaxpwlemnfac  12967  sqrtrirr  13005  odzdvds  13044  pclem0  13085  pclemub  13086  pclemdc  13087  pcprecl  13088  pcprendvds  13089  pcpremul  13092  pceulem  13093  pcval  13095  pcelnn  13120  pc2dvds  13129  pcadd  13139  pcadd2  13140  pcmpt  13142  prmpwdvds  13154  4sqlem17  13206  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemodife  13289  ballotfilemic  13299  ballotfilemsv  13302  ballotfilemrc  13323  imasaddfnlemg  13684  znf1o  15035  znidomb  15042  mplsubgfilemm  15138  mplsubgfilemcl  15139  blfvalps  15535  elblps  15540  elbl  15541  elbl3ps  15544  elbl3  15545  blres  15584  comet  15649  bdbl  15653  xmetxp  15657  xmetxpbl  15658  metcnp2  15663  txmetcnp  15668  cnbl0  15684  cnblcld  15685  bl2ioo  15700  addcncntoplem  15711  divcnap  15715  mpomulcn  15716  elcncf  15723  elcncf2  15724  cncfi  15728  rescncf  15731  mulc1cncf  15739  cncfco  15741  cncfmet  15742  cncfmptid  15747  addccncf  15750  cdivcncfap  15754  negcncf  15755  mulcncflem  15757  mulcncf  15758  ivthinclemlm  15784  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemdisj  15790  ivthinclemloc  15791  ivthinc  15793  ivthreinc  15795  limccl  15809  ellimc3apf  15810  limcdifap  15812  limcmpted  15813  limcimolemlt  15814  limcresi  15816  cnplimcim  15817  limccnpcntop  15825  limccnp2lem  15826  limccoap  15828  dvcoapbr  15857  dveflem  15876  eflt  15925  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  logltb  16026  logge0b  16042  loggt0b  16043  zprmlogbaplem2  16135  zprmlogbap  16137  pellexlem3  16150  prmefexple  16206  bposlem1  16209  lgslem2  16218  lgslem3  16219  lgsval  16221  lgsfcl2  16223  lgsfle1  16226  lgsle1  16232  lgsdirprm  16251  lgsne0  16255  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  gausslemma2dlem2  16279  gausslemma2dlem3  16280  gausslemma2dlem4  16281  subupgr  16612  vtxdumgrfival  16637  qdencn  17170  trilpolemlt1  17188