Theorem breqtrd 4030

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 4016	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶))
4	1, 3	mpbid 147	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1353   class class class wbr 4004

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005

This theorem is referenced by:  breqtrrd  4032  breqtrid  4041  tfrexlem  6335  phplem4  6855  phplem4on  6867  fidifsnen  6870  fisbth  6883  fin0  6885  fin0or  6886  ltsonq  7397  addlocprlemeqgt  7531  prmuloclemcalc  7564  mullocprlem  7569  addcanprlemu  7614  ltaprlem  7617  ltaprg  7618  prplnqu  7619  ltmprr  7641  cauappcvgprlemopl  7645  cauappcvgprlemloc  7651  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  cauappcvgprlem1  7658  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemloc  7674  caucvgprprlemloccalc  7683  caucvgprprlemopl  7696  recexgt0sr  7772  ltm1sr  7776  prsrpos  7784  caucvgsrlemoffgt1  7798  caucvgsr  7801  suplocsrlempr  7806  pitoregt0  7848  axpre-suploclemres  7900  add20  8431  mullt0  8437  ltmul1a  8548  ltm1  8803  recgt0  8807  prodgt0gt0  8808  prodgt0  8809  prodge0  8811  lemul1a  8815  recp1lt1  8856  recreclt  8857  ledivp1  8860  mulle0r  8901  ltaddrp2d  9731  mul2lt0np  9763  xleadd1a  9873  xleaddadd  9887  fz01en  10053  fzonmapblen  10187  qbtwnrelemcalc  10256  flqaddz  10297  flhalf  10302  flqdiv  10321  modqmuladdim  10367  modqsubdir  10393  addmodlteq  10398  frecfzen2  10427  iseqf1olemab  10489  ser3le  10518  ltexp2a  10572  leexp2a  10573  exple1  10576  expubnd  10577  bernneq  10641  faclbnd6  10724  hashfz  10801  zfz1isolemiso  10819  zfz1iso  10821  seq3coll  10822  cvg1nlemcxze  10991  cvg1nlemres  10994  recvguniqlem  11003  resqrexlemover  11019  resqrexlemdec  11020  resqrexlemcalc2  11024  resqrexlemcalc3  11025  resqrexlemnm  11027  resqrexlemoverl  11030  ltabs  11096  abslt  11097  absle  11098  abstri  11113  maxabslemlub  11216  maxabslemval  11217  dfabsmax  11226  bdtrilem  11247  xrmaxiflemab  11255  xrmaxiflemlub  11256  xrmaxaddlem  11268  reccn2ap  11321  climge0  11333  climaddc2  11338  summodclem2a  11389  zsumdc  11392  isumge0  11438  fsumle  11471  fsumlt  11472  isumshft  11498  expcnvap0  11510  geolim  11519  geolim2  11520  georeclim  11521  geo2lim  11524  cvgratnnlembern  11531  cvgratnnlemfm  11537  mertenslemi1  11543  mertensabs  11545  prodmodclem3  11583  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  efcllemp  11666  ef0lem  11668  efgt0  11692  eftlub  11698  efltim  11706  sinbnd  11760  cosbnd  11761  ef01bndlem  11764  sin01gt0  11769  cos01gt0  11770  sin02gt0  11771  eirraplem  11784  dvdssub2  11842  dvdsadd2b  11847  dvdsexp  11867  opoe  11900  divalglemeunn  11926  divalglemex  11927  divalglemeuneg  11928  gcdaddm  11985  bezoutlemstep  11998  dvdsgcd  12013  dvdsmulgcd  12026  bezoutr1  12034  nn0seqcvgd  12041  rpmulgcd2  12095  qredeq  12096  rpdvds  12099  prmind2  12120  divdenle  12197  phicl2  12214  hashdvds  12221  phimullem  12225  eulerthlemth  12232  prmdiveq  12236  prmdivdiv  12237  pythagtriplem4  12268  pythagtriplem10  12269  pythagtriplem19  12282  pcpre1  12292  qexpz  12350  expnprm  12351  oddprmdvds  12352  pockthlem  12354  4sqlem7  12382  4sqlem10  12385  ennnfonelemkh  12413  ennnfonelemnn0  12423  dvdsrid  13269  dvdsrtr  13270  dvdsrneg  13272  unitmulcl  13282  unitgrp  13285  unitnegcl  13299  subrguss  13357  subrgunit  13360  psmetsym  13832  psmettri  13833  mettri2  13865  xmetsym  13871  xmettri  13875  metrtri  13880  xblss2ps  13907  xblss2  13908  blhalf  13911  xmsge0  13970  cnmet  14033  ivthinclemlopn  14117  dveflem  14190  dvef  14191  sin0pilem1  14205  sinq12gt0  14254  sinq34lt0t  14255  cosq14gt0  14256  coseq0q4123  14258  rpabscxpbnd  14362  logbgcd1irraplemexp  14389  lgslem1  14404  lgseisenlem2  14454  2sqlem3  14467  2sqlem4  14468  2sqlem8  14473  pwf1oexmid  14752  qdencn  14778  cvgcmp2nlemabs  14783  apdifflemf  14797  apdifflemr  14798