Theorem breqtrrd 4159

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

Hypotheses

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

Assertion

Ref	Expression
breqtrrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrrd

Step	Hyp	Ref	Expression
1		breqtrrd.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2244	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	breqtrd 4157	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1402   class class class wbr 4131

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4132

This theorem is used by:  frirrg  4497  fidcen  7207  unsnfidcex  7231  unsnfidcel  7232  addlocprlemeq  7906  ltexprlemopl  7974  recexprlemloc  8004  cauappcvgprlemopl  8019  cauappcvgprlemladdfu  8027  cauappcvgprlem1  8032  caucvgprlemopl  8042  caucvgprlemladdfu  8050  caucvgprprlemopl  8070  caucvgprprlemexbt  8079  mulgt0sr  8151  archsr  8155  caucvgsrlemoffgt1  8172  suplocsrlemb  8179  suplocsrlem  8181  mulap0r  8951  prodgt0  9190  div4p1lem1div2  9570  mul2lt0rgt0  10178  xnn0dcle  10221  xnn0letri  10222  xleadd1a  10292  xltadd1  10295  xlt2add  10299  xposdif  10301  xlesubadd  10302  xleaddadd  10306  uzsubsubfz  10469  fzctr  10557  subfzo0  10678  exbtwnzlemstep  10699  exbtwnzlemex  10701  rebtwn2zlemstep  10704  rebtwn2z  10706  qbtwnxr  10709  xqltnle  10719  fldiv4lem1div2uz2  10762  ceilqge  10768  modqge0  10790  modqlt  10791  modqid  10807  m1modge3gt1  10829  modaddmodup  10845  addmodlteq  10856  ser3mono  10945  seqf1oglem1  10977  seqf1oglem2  10978  ser3ge0  10994  ser3le  10995  leexp1a  11052  sqgt0ap  11066  sqge0  11074  nnlesq  11101  expnbnd  11122  nn0sqdc  11168  nn0opthlem2d  11181  facwordi  11200  bcm1n  11229  filtinf  11252  hashunlem  11266  zfz1isolemiso  11313  cats1fvd  11560  cjmulge0  11676  resqrexlemover  11798  resqrexlemdec  11799  resqrexlemlo  11801  resqrexlemcalc3  11804  resqrexlemcvg  11807  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemga  11811  absge0  11848  amgm2  11907  maxle1  12000  bdtrilem  12030  xrmaxifle  12037  xrmaxiflemlub  12039  xrmaxiflemval  12041  xrmax1sup  12044  xrmaxltsup  12049  xrmaxadd  12052  xrbdtri  12067  reccn2ap  12104  climle  12125  climserle  12136  isumclim2  12214  isumclim3  12215  isumge0  12222  fsumlessfi  12252  expcnvap0  12294  expcnvre  12295  explecnv  12297  absltap  12301  cvgratnnlembern  12315  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratnnlemabsle  12319  cvgratnnlemfm  12321  cvgratnnlemrate  12322  mertenslemi1  12327  mertenslem2  12328  clim2divap  12332  prodmodclem3  12367  efcvg  12458  ege2le3  12463  efaddlem  12466  eftlub  12482  effsumlt  12484  ef01bndlem  12548  sin02gt0  12556  eirrap  12570  iddvdsexp  12607  dvdsadd  12628  dvdsfac  12652  dvdsmod  12654  3dvds  12656  omoe  12688  divalglemnn  12710  divalglemnqt  12712  flodddiv4t2lthalf  12731  bitsfzo  12747  bitsmod  12748  bitscmp  12750  bitsinv1lem  12753  dvdslegcd  12766  dfgcd3  12812  dvdssqim  12826  dvdsmulgcd  12827  nn0seqcvgd  12844  dvdslcm  12872  lcmgcdlem  12880  mulgcddvds  12897  qredeq  12899  cncongr2  12907  sqnprm  12940  isprm6  12951  sqpweven  12980  znege1  12983  sqrt2irrap  12985  nonsq  13012  hashdvds  13028  prmdiv  13042  odzdvds  13053  pythagtriplem4  13076  pcpre1  13100  pcdvdsb  13128  pcz  13140  pcprmpw2  13141  pcaddlem  13147  pcadd  13148  pcadd2  13149  pcmpt  13151  pcmptdvds  13153  fldivp1  13156  pcfaclem  13157  pockthlem  13164  4sqlem6  13191  4sqlem8  13193  4sqexercise1  13206  4sqexercise2  13207  4sqlemsdc  13208  4sqlem11  13209  4sqlem12  13210  4sqlem14  13212  4sqlem16  13214  ballotfilemsgt1  13312  ballotfilemsel1i  13314  ennnfonelemkh  13361  nninfdclemp1  13399  eqgen  14089  dvdsrmul1  14518  unitmulclb  14530  subrguss  14653  znidom  15101  znunit  15103  mplsubgfilemcl  15215  psmetxrge0  15558  isxmet2d  15574  mettri  15599  xmettri3  15600  mettri3  15601  xblss2ps  15630  blss2ps  15632  blss2  15633  blssps  15653  blss  15654  xmetxp  15733  ivthdec  15870  ivthreinc  15871  hoverb  15874  hovergt0  15876  sin0pilem1  16008  sinq12gt0  16057  tangtx  16065  cosordlem  16077  cosq34lt1  16078  logdivlti  16111  logbgcd1irrap  16206  birthdaylem3  16227  chtqge0  16247  chtublem  16295  perfectlem1  16299  bcmax  16305  bposlem1  16311  bposlem2  16312  bposlem5  16315  bposlem6  16316  bposlem7  16317  lgsdilem2  16360  gausslemma2dlem1f1o  16384  lgsquadlem1  16401  2lgsoddprmlem2  16430  2sqlem3  16441  2sqlem8  16447  usgrsizedgen  16659  cvgcmp2nlemabs  17287  trilpolemclim  17292  trilpolemeq1  17296  apdifflemf  17302  apdifflemr  17303  nconstwlpolemgt0  17321