Theorem breq1d 3830

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

Syntax hints:   → wi 4   ↔ wb 103   = wceq 1287   class class class wbr 3820

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-br 3821

This theorem is referenced by:  eqbrtrd  3840  syl6eqbr  3857  sbcbr2g  3872  pofun  4113  fmptco  5427  isorel  5548  isocnv  5551  isotr  5556  caovordig  5767  caovordg  5769  caovord  5773  xporderlem  5953  reldmtpos  5972  brtposg  5973  tpostpos  5983  tposoprab  5999  th3qlem2  6347  ensn1g  6466  fndmeng  6479  xpsneng  6490  xpcomco  6494  snnen2oprc  6528  tridc  6567  fimax2gtrilemstep  6568  unsnfidcel  6583  pm54.43  6762  ltsonq  6901  ltanqg  6903  ltmnqg  6904  archnqq  6920  prloc  6994  addnqprulem  7031  appdivnq  7066  mulnqpru  7072  mullocprlem  7073  1idpru  7094  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemlol  7150  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlemladdfl  7158  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  cauappcvgprlem1  7162  cauappcvgprlem2  7163  cauappcvgprlemlim  7164  cauappcvgpr  7165  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemcl  7179  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprlem1  7182  caucvgprlem2  7183  caucvgpr  7185  caucvgprprlemell  7188  caucvgprprlemelu  7189  caucvgprprlemcbv  7190  caucvgprprlemval  7191  caucvgprprlemnkltj  7192  caucvgprprlemnkeqj  7193  caucvgprprlemnbj  7196  caucvgprprlemml  7197  caucvgprprlemmu  7198  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemopu  7202  caucvgprprlemloc  7206  caucvgprprlemclphr  7208  caucvgprprlemexbt  7209  caucvgprprlemexb  7210  caucvgprprlemaddq  7211  caucvgprprlem1  7212  caucvgprprlem2  7213  ltsosr  7254  ltasrg  7260  addgt0sr  7265  mulextsr1  7270  prsrlt  7276  caucvgsrlemgt1  7284  caucvgsrlemoffres  7289  caucvgsr  7291  pitonnlem2  7328  pitonn  7329  recidpipr  7337  axpre-ltadd  7365  axpre-mulext  7367  nntopi  7373  axcaucvglemval  7376  axcaucvglemcau  7377  axcaucvglemres  7378  ltaddnegr  7847  ltsubadd  7854  lesubadd  7856  ltaddsub2  7859  leaddsub2  7861  ltaddpos  7874  lesub2  7879  ltsub2  7881  ltnegcon2  7886  lenegcon2  7889  addge01  7894  subge0  7897  suble0  7898  lesub0  7901  apreap  8005  divap0b  8089  mulgt1  8259  ltmulgt11  8260  gt0div  8266  ge0div  8267  ltmuldiv  8270  ltmuldiv2  8271  lemuldiv2  8278  ltrec  8279  lerec2  8285  ltdiv23  8288  lediv23  8289  addltmul  8585  avglt1  8587  avgle1  8589  div4p1lem1div2  8602  ztri3or  8726  zlem1lt  8739  zgt0ge1  8741  qapne  9056  divlt1lt  9133  divle1le  9134  xrltso  9198  xltnegi  9229  nn0disj  9477  qavgle  9598  frec2uzf1od  9741  iseqf1olemfvp  9830  expivallem  9854  expap0  9883  leexp2r  9907  sqap0  9919  nn0opthlem1d  10024  hashennnuni  10083  hashunlem  10108  zfz1isolemiso  10140  iseqcoll  10143  shftfvalg  10148  shftfibg  10150  shftfval  10151  shftfib  10153  shftfn  10154  2shfti  10161  shftidt2  10162  caucvgre  10309  cvg1nlemcau  10312  cvg1nlemres  10313  resqrexlemdecn  10340  resqrexlemoverl  10349  resqrexlemglsq  10350  resqrexlemsqa  10352  resqrexlemex  10353  abs00ap  10390  absdiflt  10420  absdifle  10421  lenegsq  10423  cau3lem  10442  minmax  10554  clim  10562  clim2  10564  clim0  10566  clim0c  10567  climi0  10570  climuni  10574  2clim  10582  climshftlemg  10583  climshft  10585  climabs0  10588  climcn1  10589  climcn2  10590  addcn2  10591  subcn2  10592  mulcn2  10593  climcau  10626  serif0  10631  sumeq1  10634  sumeq2  10638  isumrb  10657  isummolem2  10661  isummo  10662  zisum  10663  halfleoddlt  10769  gcddvds  10830  dvdssq  10895  lcmgcdlem  10934  lcmdvds  10936  isprm  10966  prmgt1  10988  isprm6  11001  pw2dvdslemn  11018  pw2dvdseu  11021  oddpwdclemxy  11022  oddpwdclemndvds  11024  oddpwdclemodd  11025  qdencn  11353