Theorem breqtrrd 3840

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 2090	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	breqtrd 3838	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1287   class class class wbr 3814

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 2616  df-un 2990  df-sn 3431  df-pr 3432  df-op 3434  df-br 3815

This theorem is referenced by:  frirrg  4144  unsnfidcex  6560  unsnfidcel  6561  addlocprlemeq  7013  ltexprlemopl  7081  recexprlemloc  7111  cauappcvgprlemopl  7126  cauappcvgprlemladdfu  7134  cauappcvgprlem1  7139  caucvgprlemopl  7149  caucvgprlemladdfu  7157  caucvgprprlemopl  7177  caucvgprprlemexbt  7186  mulgt0sr  7244  archsr  7248  caucvgsrlemoffgt1  7265  mulap0r  8010  prodgt0  8225  div4p1lem1div2  8579  uzsubsubfz  9370  fzctr  9449  subfzo0  9556  exbtwnzlemstep  9562  exbtwnzlemex  9564  rebtwn2zlemstep  9567  rebtwn2z  9569  qbtwnxr  9572  ceilqge  9620  modqge0  9642  modqlt  9643  modqid  9659  m1modge3gt1  9681  modaddmodup  9697  addmodlteq  9708  isermono  9786  serile  9804  leexp1a  9861  sqgt0ap  9874  sqge0  9882  nnlesq  9908  expnbnd  9926  nn0opthlem2d  9978  facwordi  9997  filtinf  10049  hashunlem  10061  cjmulge0  10164  resqrexlemover  10284  resqrexlemdec  10285  resqrexlemlo  10287  resqrexlemcalc3  10290  resqrexlemcvg  10293  resqrexlemoverl  10295  resqrexlemglsq  10296  resqrexlemga  10297  absge0  10334  amgm2  10392  maxle1  10485  climle  10560  climserile  10571  iddvdsexp  10614  dvdsadd  10633  dvdsfac  10655  dvdsmod  10657  omoe  10690  divalglemnn  10712  divalglemnqt  10714  flodddiv4t2lthalf  10731  dvdslegcd  10750  dfgcd3  10793  dvdssqim  10807  dvdsmulgcd  10808  nn0seqcvgd  10817  dvdslcm  10845  lcmgcdlem  10853  mulgcddvds  10870  qredeq  10872  cncongr2  10880  sqnprm  10911  isprm6  10920  sqpweven  10947  znege1  10950  sqrt2irrap  10952  nonsq  10979  hashdvds  10991