Theorem eqbrtrrd 4155

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 2244	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqbrtrrd.2	. 2 ⊢ (𝜑 → 𝐴𝑅𝐶)
4	2, 3	eqbrtrd 4153	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:  dftpos4  6538  phpm  7171  unsnfidcex  7231  fisseneq  7246  f1finf1o  7269  prmuloclemcalc  7938  mullocprlem  7943  cauappcvgprlemladdfl  8028  caucvgprlemopl  8042  caucvgprprlemloccalc  8057  caucvgprprlemopl  8070  ltadd1sr  8149  suplocsrlem  8181  axarch  8264  axpre-suploclemres  8274  lemulge11  9204  mul2lt0llt0  10179  mul2lt0lgt0  10180  mul2lt0pn  10182  xaddge0  10297  modqmuladdim  10825  ltexp2a  11049  leexp2a  11050  nnlesq  11101  faclbnd6  11204  facavg  11206  bcm1n  11229  fiprsshashgt1  11280  sseqn  11301  sq01  11682  cvg1nlemcxze  11770  resqrexlemover  11798  resqrexlemlo  11801  resqrexlemnmsq  11805  resqrexlemnm  11806  leabs  11862  abs3dif  11894  abs2dif  11895  maxabslemlub  11996  maxltsup  12007  bdtri  12031  xrmaxiflemab  12038  xrbdtri  12067  recn2  12108  imcn2  12109  iserex  12130  summodclem2a  12173  fsumge1  12253  isumrpcl  12286  cvgratnnlemseq  12318  cvgratnnlemsumlt  12320  mertenslemi1  12327  prodmodclem2a  12368  ege2le3  12463  efgt1p2  12487  efgt1p  12488  tanval2ap  12505  tanval3ap  12506  cos12dec  12560  eirraplem  12569  fsumdvds  12634  divalglemnqt  12712  bitsfzo  12747  bitsmod  12748  bitscmp  12750  mulgcd  12818  dvdssqlem  12832  nn0seqcvgd  12844  mulgcddvds  12897  rpdvds  12902  isprm5  12946  pwbdvdseulemle  12971  sqrt2irraplemnn  12984  qden1elz  13010  phimullem  13032  hashgcdlem  13045  hashgcdeq  13047  pceu  13103  pcdvdstr  13135  pockthg  13165  4sqlem11  13209  ennnfonelemex  13363  znrrg  15104  lmcn2  15506  psmetge0  15557  xmetge0  15591  cnopnap  15837  suplociccex  15851  ivthinclemlopn  15862  ivthinclemuopn  15864  hoverb  15874  ivthdichlem  15877  cnplimclemr  15895  limccnp2lem  15902  dveflem  15952  efltlemlt  16000  cosq23lt0  16060  coseq0q4123  16061  cosq34lt1  16078  logdivlti  16111  logdivlt  16124  ppiqltx  16281  chtqub  16296  bcmono  16304  bposlem2  16312  bposlem5  16315  bposlem6  16316  lgsne0  16362  lgsquadlem1  16401  lgsquadlem2  16402  umgrnloopv  16560  umgredgprv  16561  upgr1een  16570  1hegrvtxdg1fi  16755  apdiff  17304  taupi  17330