Theorem eqbrtrrd 4117

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 2237	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqbrtrrd.2	. 2 ⊢ (𝜑 → 𝐴𝑅𝐶)
4	2, 3	eqbrtrd 4115	1 ⊢ (𝜑 → 𝐵𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1398   class class class wbr 4093

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094

This theorem is referenced by:  dftpos4  6472  phpm  7095  unsnfidcex  7155  fisseneq  7170  f1finf1o  7189  prmuloclemcalc  7828  mullocprlem  7833  cauappcvgprlemladdfl  7918  caucvgprlemopl  7932  caucvgprprlemloccalc  7947  caucvgprprlemopl  7960  ltadd1sr  8039  suplocsrlem  8071  axarch  8154  axpre-suploclemres  8164  lemulge11  9088  mul2lt0llt0  10040  mul2lt0lgt0  10041  mul2lt0pn  10043  xaddge0  10157  modqmuladdim  10675  ltexp2a  10899  leexp2a  10900  nnlesq  10951  faclbnd6  11052  facavg  11054  fiprsshashgt1  11127  cvg1nlemcxze  11605  resqrexlemover  11633  resqrexlemlo  11636  resqrexlemnmsq  11640  resqrexlemnm  11641  leabs  11697  abs3dif  11728  abs2dif  11729  maxabslemlub  11830  maxltsup  11841  bdtri  11863  xrmaxiflemab  11870  xrbdtri  11899  recn2  11940  imcn2  11941  iserex  11962  summodclem2a  12005  fsumge1  12085  isumrpcl  12118  cvgratnnlemseq  12150  cvgratnnlemsumlt  12152  mertenslemi1  12159  prodmodclem2a  12200  ege2le3  12295  efgt1p2  12319  efgt1p  12320  tanval2ap  12337  tanval3ap  12338  cos12dec  12392  eirraplem  12401  fsumdvds  12466  divalglemnqt  12544  bitsfzo  12579  bitsmod  12580  bitscmp  12582  mulgcd  12650  dvdssqlem  12664  nn0seqcvgd  12676  mulgcddvds  12729  rpdvds  12734  isprm5  12777  pw2dvdseulemle  12802  sqrt2irraplemnn  12814  qden1elz  12840  phimullem  12860  hashgcdlem  12873  hashgcdeq  12875  pceu  12931  pcdvdstr  12963  pockthg  12993  4sqlem11  13037  ennnfonelemex  13098  znrrg  14739  lmcn2  15074  psmetge0  15125  xmetge0  15159  cnopnap  15405  suplociccex  15419  ivthinclemlopn  15430  ivthinclemuopn  15432  hoverb  15442  ivthdichlem  15445  cnplimclemr  15463  limccnp2lem  15470  dveflem  15520  efltlemlt  15568  cosq23lt0  15627  coseq0q4123  15628  cosq34lt1  15644  logdivlti  15675  lgsne0  15840  lgsquadlem1  15879  lgsquadlem2  15880  umgrnloopv  16038  umgredgprv  16039  upgr1een  16048  1hegrvtxdg1fi  16233  apdiff  16763  taupi  16789