Theorem breq1d 4096

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

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

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  eqnbrtrd  4104  eqbrtrd  4108  eqbrtrdi  4125  sbcbr2g  4144  pofun  4407  fmptco  5809  isorel  5944  isocnv  5947  isotr  5952  imbrov2fvoveq  6038  caovordig  6183  caovordg  6185  caovord  6189  xporderlem  6391  reldmtpos  6414  brtposg  6415  tpostpos  6425  tposoprab  6441  th3qlem2  6802  ensn1g  6966  fndmeng  6980  xpsneng  7001  xpcomco  7005  snnen2oprc  7041  tridc  7082  fimax2gtrilemstep  7083  unsnfidcel  7106  pm54.43  7386  pr1or2  7390  ccfunen  7473  ltsonq  7608  ltanqg  7610  ltmnqg  7611  archnqq  7627  prloc  7701  addnqprulem  7738  appdivnq  7773  mulnqpru  7779  mullocprlem  7780  1idpru  7801  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlemladdfl  7865  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem1  7869  cauappcvgprlem2  7870  cauappcvgprlemlim  7871  cauappcvgpr  7872  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemcl  7886  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  caucvgprlem1  7889  caucvgprlem2  7890  caucvgpr  7892  caucvgprprlemell  7895  caucvgprprlemelu  7896  caucvgprprlemcbv  7897  caucvgprprlemval  7898  caucvgprprlemnkltj  7899  caucvgprprlemnkeqj  7900  caucvgprprlemnbj  7903  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemopu  7909  caucvgprprlemloc  7913  caucvgprprlemclphr  7915  caucvgprprlemexbt  7916  caucvgprprlemexb  7917  caucvgprprlemaddq  7918  caucvgprprlem1  7919  caucvgprprlem2  7920  ltsosr  7974  ltasrg  7980  addgt0sr  7985  mulextsr1  7991  prsrlt  7997  caucvgsrlemgt1  8005  caucvgsrlemoffres  8010  caucvgsr  8012  ltpsrprg  8013  pitonnlem2  8057  pitonn  8058  recidpipr  8066  axpre-ltadd  8096  axpre-mulext  8098  nntopi  8104  axcaucvglemval  8107  axcaucvglemcau  8108  axcaucvglemres  8109  ltaddnegr  8595  ltsubadd  8602  lesubadd  8604  ltaddsub2  8607  leaddsub2  8609  ltaddpos  8622  lesub2  8627  ltsub2  8629  ltnegcon2  8634  lenegcon2  8637  addge01  8642  subge0  8645  suble0  8646  lesub0  8649  ltordlem  8652  apreap  8757  divap0b  8853  mulgt1  9033  ltmulgt11  9034  gt0div  9040  ge0div  9041  ltmuldiv  9044  ltmuldiv2  9045  lemuldiv2  9052  ltrec  9053  lerec2  9059  ltdiv23  9062  lediv23  9063  sup3exmid  9127  addltmul  9371  avglt1  9373  avgle1  9375  div4p1lem1div2  9388  ztri3or  9512  zlem1lt  9526  zgt0ge1  9528  qapne  9863  irrmulap  9872  divlt1lt  9949  divle1le  9950  xrltso  10021  xltnegi  10060  xltadd1  10101  xposdif  10107  xlesubadd  10108  xleaddadd  10112  nn0disj  10363  qavgle  10508  fldiv4lem1div2uz2  10556  frec2uzf1od  10658  iseqf1olemfvp  10762  seqf1oglem1  10771  exp3vallem  10792  expap0  10821  leexp2r  10845  sqap0  10858  nn0ltexp2  10961  nn0opthlem1d  10972  hashennnuni  11031  hashunlem  11057  zfz1isolemiso  11093  seq3coll  11096  swrdccatin2  11300  shftfvalg  11369  shftfibg  11371  shftfval  11372  shftfib  11374  shftfn  11375  2shfti  11382  shftidt2  11383  caucvgre  11532  cvg1nlemcau  11535  cvg1nlemres  11536  resqrexlemdecn  11563  resqrexlemoverl  11572  resqrexlemglsq  11573  resqrexlemsqa  11575  resqrexlemex  11576  abs00ap  11613  absdiflt  11643  absdifle  11644  lenegsq  11646  cau3lem  11665  minmax  11781  xrmaxltsup  11809  xrminmax  11816  xrltmininf  11821  xrlemininf  11822  clim  11832  clim2  11834  clim0  11836  clim0c  11837  climi0  11840  climuni  11844  2clim  11852  climshftlemg  11853  climshft  11855  climabs0  11858  climcn1  11859  climcn2  11860  addcn2  11861  subcn2  11862  mulcn2  11863  iser3shft  11897  climcau  11898  serf0  11903  sumeq1  11906  sumeq2  11910  sumrbdc  11930  summodclem2  11933  summodc  11934  zsumdc  11935  isumshft  12041  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  prodfap0  12096  prodfrecap  12097  prodfdivap  12098  ntrivcvgap  12099  ntrivcvgap0  12100  prodeq1f  12103  prodeq2w  12107  prodeq2  12108  prodrbdclem2  12124  prodmodclem2  12128  prodmodc  12129  zproddc  12130  fprodntrivap  12135  fprodap0  12172  fprodrec  12180  fproddivapf  12182  fprodap0f  12187  tanaddaplem  12289  sin01bnd  12308  cos01bnd  12309  halfleoddlt  12445  gcddvds  12524  dvdssq  12592  lcmgcdlem  12639  lcmdvds  12641  isprm  12671  prmgt1  12694  isprm5lem  12703  isprm6  12709  pw2dvdslemn  12727  pw2dvdseu  12730  oddpwdclemxy  12731  oddpwdclemndvds  12733  oddpwdclemodd  12734  odzdvds  12808  pclem0  12849  pclemub  12850  pclemdc  12851  pcprecl  12852  pcprendvds  12853  pcpremul  12856  pceulem  12857  pcval  12859  pcelnn  12884  pc2dvds  12893  pcadd  12903  pcadd2  12904  pcmpt  12906  prmpwdvds  12918  4sqlem17  12970  imasaddfnlemg  13387  znf1o  14655  znidomb  14662  mplsubgfilemm  14702  mplsubgfilemcl  14703  blfvalps  15099  elblps  15104  elbl  15105  elbl3ps  15108  elbl3  15109  blres  15148  comet  15213  bdbl  15217  xmetxp  15221  xmetxpbl  15222  metcnp2  15227  txmetcnp  15232  cnbl0  15248  cnblcld  15249  bl2ioo  15264  addcncntoplem  15275  divcnap  15279  mpomulcn  15280  elcncf  15287  elcncf2  15288  cncfi  15292  rescncf  15295  mulc1cncf  15303  cncfco  15305  cncfmet  15306  cncfmptid  15311  addccncf  15314  cdivcncfap  15318  negcncf  15319  mulcncflem  15321  mulcncf  15322  ivthinclemlm  15348  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemdisj  15354  ivthinclemloc  15355  ivthinc  15357  ivthreinc  15359  limccl  15373  ellimc3apf  15374  limcdifap  15376  limcmpted  15377  limcimolemlt  15378  limcresi  15380  cnplimcim  15381  limccnpcntop  15389  limccnp2lem  15390  limccoap  15392  dvcoapbr  15421  dveflem  15440  eflt  15489  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  logltb  15588  logge0b  15604  loggt0b  15605  lgslem2  15720  lgslem3  15721  lgsval  15723  lgsfcl2  15725  lgsfle1  15728  lgsle1  15734  lgsdirprm  15753  lgsne0  15757  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  gausslemma2dlem2  15781  gausslemma2dlem3  15782  gausslemma2dlem4  15783  vtxdumgrfival  16104  qdencn  16567  trilpolemlt1  16581