Theorem eqbrtrrd 4106

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

Hypotheses

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

Assertion

Ref	Expression
eqbrtrrd	⊢ (𝜑 → 𝐵𝑅𝐶)

Proof of Theorem eqbrtrrd

Step	Hyp	Ref	Expression
1		eqbrtrrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqcomd 2235	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqbrtrrd.2	. 2 ⊢ (𝜑 → 𝐴𝑅𝐶)
4	2, 3	eqbrtrd 4104	1 ⊢ (𝜑 → 𝐵𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1395   class class class wbr 4082

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4083

This theorem is referenced by:  dftpos4  6407  phpm  7023  unsnfidcex  7078  fisseneq  7092  f1finf1o  7110  prmuloclemcalc  7748  mullocprlem  7753  cauappcvgprlemladdfl  7838  caucvgprlemopl  7852  caucvgprprlemloccalc  7867  caucvgprprlemopl  7880  ltadd1sr  7959  suplocsrlem  7991  axarch  8074  axpre-suploclemres  8084  lemulge11  9009  mul2lt0llt0  9953  mul2lt0lgt0  9954  mul2lt0pn  9956  xaddge0  10070  modqmuladdim  10584  ltexp2a  10808  leexp2a  10809  nnlesq  10860  faclbnd6  10961  facavg  10963  fiprsshashgt1  11034  cvg1nlemcxze  11488  resqrexlemover  11516  resqrexlemlo  11519  resqrexlemnmsq  11523  resqrexlemnm  11524  leabs  11580  abs3dif  11611  abs2dif  11612  maxabslemlub  11713  maxltsup  11724  bdtri  11746  xrmaxiflemab  11753  xrbdtri  11782  recn2  11823  imcn2  11824  iserex  11845  summodclem2a  11887  fsumge1  11967  isumrpcl  12000  cvgratnnlemseq  12032  cvgratnnlemsumlt  12034  mertenslemi1  12041  prodmodclem2a  12082  ege2le3  12177  efgt1p2  12201  efgt1p  12202  tanval2ap  12219  tanval3ap  12220  cos12dec  12274  eirraplem  12283  fsumdvds  12348  divalglemnqt  12426  bitsfzo  12461  bitsmod  12462  bitscmp  12464  mulgcd  12532  dvdssqlem  12546  nn0seqcvgd  12558  mulgcddvds  12611  rpdvds  12616  isprm5  12659  pw2dvdseulemle  12684  sqrt2irraplemnn  12696  qden1elz  12722  phimullem  12742  hashgcdlem  12755  hashgcdeq  12757  pceu  12813  pcdvdstr  12845  pockthg  12875  4sqlem11  12919  ennnfonelemex  12980  znrrg  14618  lmcn2  14948  psmetge0  14999  xmetge0  15033  cnopnap  15279  suplociccex  15293  ivthinclemlopn  15304  ivthinclemuopn  15306  hoverb  15316  ivthdichlem  15319  cnplimclemr  15337  limccnp2lem  15344  dveflem  15394  efltlemlt  15442  cosq23lt0  15501  coseq0q4123  15502  cosq34lt1  15518  logdivlti  15549  lgsne0  15711  lgsquadlem1  15750  lgsquadlem2  15751  umgrnloopv  15908  umgredgprv  15909  apdiff  16375  taupi  16400