Theorem breqtrd 3809

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)

Hypotheses

Ref	Expression
breqtrd.1	⊢ (𝜑 → 𝐴𝑅𝐵)
breqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
breqtrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrd

Step	Hyp	Ref	Expression
1		breqtrd.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	breq2d 3797	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶))
4	1, 3	mpbid 145	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1284   class class class wbr 3785

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 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-br 3786

This theorem is referenced by:  breqtrrd  3811  syl5breq  3820  tfrexlem  5971  phplem4  6341  phplem4on  6353  fidifsnen  6355  fisbth  6367  fin0  6369  fin0or  6370  ltsonq  6588  addlocprlemeqgt  6722  prmuloclemcalc  6755  mullocprlem  6760  addcanprlemu  6805  ltaprlem  6808  ltaprg  6809  prplnqu  6810  ltmprr  6832  cauappcvgprlemopl  6836  cauappcvgprlemloc  6842  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem1  6849  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemloc  6865  caucvgprprlemloccalc  6874  caucvgprprlemopl  6887  recexgt0sr  6950  prsrpos  6961  caucvgsrlemoffgt1  6975  caucvgsr  6978  pitoregt0  7017  add20  7578  mullt0  7584  ltmul1a  7691  ltm1  7924  recgt0  7928  prodgt0gt0  7929  prodgt0  7930  prodge0  7932  lemul1a  7936  recp1lt1  7977  recreclt  7978  ledivp1  7981  mulle0r  8022  ltaddrp2d  8808  fz01en  9072  fzonmapblen  9196  qbtwnrelemcalc  9264  flqaddz  9299  flhalf  9304  flqdiv  9323  modqmuladdim  9369  modqsubdir  9395  addmodlteq  9400  frecfzen2  9420  serile  9474  ltexp2a  9528  leexp2a  9529  exple1  9532  expubnd  9533  bernneq  9593  faclbnd6  9671  cvg1nlemcxze  9868  cvg1nlemres  9871  recvguniqlem  9880  resqrexlemover  9896  resqrexlemdec  9897  resqrexlemcalc2  9901  resqrexlemcalc3  9902  resqrexlemnm  9904  resqrexlemoverl  9907  ltabs  9973  abslt  9974  absle  9975  abstri  9990  maxabslemlub  10093  maxabslemval  10094  dfabsmax  10103  climge0  10163  climaddc2  10168  dvdssub2  10237  dvdsadd2b  10242  dvdsexp  10261  opoe  10295  divalglemeunn  10321  divalglemex  10322  divalglemeuneg  10323  gcdaddm  10375  bezoutlemstep  10386  dvdsgcd  10401  dvdsmulgcd  10414  bezoutr1  10422  nn0seqcvgd  10423  rpmulgcd2  10477  qredeq  10478  rpdvds  10481  prmind2  10502  qdencn  10785