Theorem breq1d 4103

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   class class class wbr 4093

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094

This theorem is referenced by:  eqnbrtrd  4111  eqbrtrd  4115  eqbrtrdi  4132  sbcbr2g  4151  pofun  4415  fmptco  5821  isorel  5959  isocnv  5962  isotr  5967  imbrov2fvoveq  6053  caovordig  6198  caovordg  6200  caovord  6204  xporderlem  6405  reldmtpos  6462  brtposg  6463  tpostpos  6473  tposoprab  6489  th3qlem2  6850  ensn1g  7014  fndmeng  7028  xpsneng  7049  xpcomco  7053  snnen2oprc  7089  tridc  7132  fimax2gtrilemstep  7133  unsnfidcel  7156  pm54.43  7438  pr1or2  7442  ccfunen  7526  ltsonq  7661  ltanqg  7663  ltmnqg  7664  archnqq  7680  prloc  7754  addnqprulem  7791  appdivnq  7826  mulnqpru  7832  mullocprlem  7833  1idpru  7854  cauappcvgprlemm  7908  cauappcvgprlemopl  7909  cauappcvgprlemlol  7910  cauappcvgprlemdisj  7914  cauappcvgprlemloc  7915  cauappcvgprlemladdfl  7918  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgprlem1  7922  cauappcvgprlem2  7923  cauappcvgprlemlim  7924  cauappcvgpr  7925  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemm  7931  caucvgprlemopl  7932  caucvgprlemlol  7933  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlemcl  7939  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgprlem1  7942  caucvgprlem2  7943  caucvgpr  7945  caucvgprprlemell  7948  caucvgprprlemelu  7949  caucvgprprlemcbv  7950  caucvgprprlemval  7951  caucvgprprlemnkltj  7952  caucvgprprlemnkeqj  7953  caucvgprprlemnbj  7956  caucvgprprlemml  7957  caucvgprprlemmu  7958  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemopu  7962  caucvgprprlemloc  7966  caucvgprprlemclphr  7968  caucvgprprlemexbt  7969  caucvgprprlemexb  7970  caucvgprprlemaddq  7971  caucvgprprlem1  7972  caucvgprprlem2  7973  ltsosr  8027  ltasrg  8033  addgt0sr  8038  mulextsr1  8044  prsrlt  8050  caucvgsrlemgt1  8058  caucvgsrlemoffres  8063  caucvgsr  8065  ltpsrprg  8066  pitonnlem2  8110  pitonn  8111  recidpipr  8119  axpre-ltadd  8149  axpre-mulext  8151  nntopi  8157  axcaucvglemval  8160  axcaucvglemcau  8161  axcaucvglemres  8162  ltaddnegr  8647  ltsubadd  8654  lesubadd  8656  ltaddsub2  8659  leaddsub2  8661  ltaddpos  8674  lesub2  8679  ltsub2  8681  ltnegcon2  8686  lenegcon2  8689  addge01  8694  subge0  8697  suble0  8698  lesub0  8701  ltordlem  8704  apreap  8809  divap0b  8905  mulgt1  9085  ltmulgt11  9086  gt0div  9092  ge0div  9093  ltmuldiv  9096  ltmuldiv2  9097  lemuldiv2  9104  ltrec  9105  lerec2  9111  ltdiv23  9114  lediv23  9115  sup3exmid  9179  addltmul  9423  avglt1  9425  avgle1  9427  div4p1lem1div2  9440  ztri3or  9566  zlem1lt  9580  zgt0ge1  9582  qapne  9917  irrmulap  9926  divlt1lt  10003  divle1le  10004  xrltso  10075  xltnegi  10114  xltadd1  10155  xposdif  10161  xlesubadd  10162  xleaddadd  10166  nn0disj  10418  qavgle  10564  fldiv4lem1div2uz2  10612  frec2uzf1od  10714  iseqf1olemfvp  10818  seqf1oglem1  10827  exp3vallem  10848  expap0  10877  leexp2r  10901  sqap0  10914  nn0ltexp2  11017  nn0opthlem1d  11028  hashennnuni  11087  hashunlem  11113  zfz1isolemiso  11149  seq3coll  11152  swrdccatin2  11359  shftfvalg  11441  shftfibg  11443  shftfval  11444  shftfib  11446  shftfn  11447  2shfti  11454  shftidt2  11455  caucvgre  11604  cvg1nlemcau  11607  cvg1nlemres  11608  resqrexlemdecn  11635  resqrexlemoverl  11644  resqrexlemglsq  11645  resqrexlemsqa  11647  resqrexlemex  11648  abs00ap  11685  absdiflt  11715  absdifle  11716  lenegsq  11718  cau3lem  11737  minmax  11853  xrmaxltsup  11881  xrminmax  11888  xrltmininf  11893  xrlemininf  11894  clim  11904  clim2  11906  clim0  11908  clim0c  11909  climi0  11912  climuni  11916  2clim  11924  climshftlemg  11925  climshft  11927  climabs0  11930  climcn1  11931  climcn2  11932  addcn2  11933  subcn2  11934  mulcn2  11935  iser3shft  11969  climcau  11970  serf0  11975  sumeq1  11978  sumeq2  11982  sumrbdc  12003  summodclem2  12006  summodc  12007  zsumdc  12008  isumshft  12114  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  prodfap0  12169  prodfrecap  12170  prodfdivap  12171  ntrivcvgap  12172  ntrivcvgap0  12173  prodeq1f  12176  prodeq2w  12180  prodeq2  12181  prodrbdclem2  12197  prodmodclem2  12201  prodmodc  12202  zproddc  12203  fprodntrivap  12208  fprodap0  12245  fprodrec  12253  fproddivapf  12255  fprodap0f  12260  tanaddaplem  12362  sin01bnd  12381  cos01bnd  12382  halfleoddlt  12518  gcddvds  12597  dvdssq  12665  lcmgcdlem  12712  lcmdvds  12714  isprm  12744  prmgt1  12767  isprm5lem  12776  isprm6  12782  pw2dvdslemn  12800  pw2dvdseu  12803  oddpwdclemxy  12804  oddpwdclemndvds  12806  oddpwdclemodd  12807  odzdvds  12881  pclem0  12922  pclemub  12923  pclemdc  12924  pcprecl  12925  pcprendvds  12926  pcpremul  12929  pceulem  12930  pcval  12932  pcelnn  12957  pc2dvds  12966  pcadd  12976  pcadd2  12977  pcmpt  12979  prmpwdvds  12991  4sqlem17  13043  imasaddfnlemg  13460  znf1o  14730  znidomb  14737  mplsubgfilemm  14782  mplsubgfilemcl  14783  blfvalps  15179  elblps  15184  elbl  15185  elbl3ps  15188  elbl3  15189  blres  15228  comet  15293  bdbl  15297  xmetxp  15301  xmetxpbl  15302  metcnp2  15307  txmetcnp  15312  cnbl0  15328  cnblcld  15329  bl2ioo  15344  addcncntoplem  15355  divcnap  15359  mpomulcn  15360  elcncf  15367  elcncf2  15368  cncfi  15372  rescncf  15375  mulc1cncf  15383  cncfco  15385  cncfmet  15386  cncfmptid  15391  addccncf  15394  cdivcncfap  15398  negcncf  15399  mulcncflem  15401  mulcncf  15402  ivthinclemlm  15428  ivthinclemlopn  15430  ivthinclemlr  15431  ivthinclemuopn  15432  ivthinclemur  15433  ivthinclemdisj  15434  ivthinclemloc  15435  ivthinc  15437  ivthreinc  15439  limccl  15453  ellimc3apf  15454  limcdifap  15456  limcmpted  15457  limcimolemlt  15458  limcresi  15460  cnplimcim  15461  limccnpcntop  15469  limccnp2lem  15470  limccoap  15472  dvcoapbr  15501  dveflem  15520  eflt  15569  sincosq2sgn  15621  sincosq3sgn  15622  sincosq4sgn  15623  logltb  15668  logge0b  15684  loggt0b  15685  pellexlem3  15776  lgslem2  15803  lgslem3  15804  lgsval  15806  lgsfcl2  15808  lgsfle1  15811  lgsle1  15817  lgsdirprm  15836  lgsne0  15840  gausslemma2dlem1a  15860  gausslemma2dlem1f1o  15862  gausslemma2dlem2  15864  gausslemma2dlem3  15865  gausslemma2dlem4  15866  subupgr  16197  vtxdumgrfival  16222  qdencn  16738  trilpolemlt1  16756