Theorem eqbrtrd 4137

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

Hypotheses

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

Assertion

Ref	Expression
eqbrtrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem eqbrtrd

Step	Hyp	Ref	Expression
1		eqbrtrd.2	. 2 ⊢ (𝜑 → 𝐵𝑅𝐶)
2		eqbrtrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	breq1d 4125	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 167	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3701  df-pr 3702  df-op 3704  df-br 4116

This theorem is referenced by:  eqbrtrrd  4139  dif1en  7151  ccfunen  7596  prarloclemcalc  7835  ltexprlemopu  7936  recexprlemloc  7964  caucvgprprlemloccalc  8017  suplocsrlem  8141  axpre-suploclemres  8234  mulle0r  9240  lbinfle  9246  divge1  10079  ltesubnnd  10125  xltnegi  10192  xleadd1a  10230  xltadd1  10233  xlt2add  10237  xposdif  10239  xleaddadd  10244  lincmble  10361  ubmelm1fzo  10598  infssfzledc  10624  zsupssdc  10627  qbtwnrelemcalc  10644  qbtwnxr  10646  ceiqm1l  10702  ceilqm1lt  10703  ceilqle  10705  modqlt  10724  modqeqmodmin  10785  addmodlteq  10789  seqf1oglem1  10910  exp3vallem  10931  bernneq  11052  nn0ltexp2  11101  faclbnd2  11134  sshashneg  11235  ccatsymb  11320  ccatrn  11327  sq01  11610  resqrexlemdec  11727  resqrexlemcalc2  11731  resqrexlemglsq  11738  resqrexlemga  11739  abslt  11804  amgm2  11834  icodiamlt  11896  maxabsle  11920  maxltsup  11934  minmax  11946  min1inf  11948  min2inf  11949  bdtrilem  11955  xrmaxltsup  11974  xrmaxaddlem  11976  xrmaxadd  11977  xrminmax  11981  xrmin1inf  11983  xrmin2inf  11984  climconst  12006  serclim0  12021  mulcn2  12028  reccn2ap  12029  iserex  12055  climlec2  12057  iserge0  12059  climcau  12063  climcvg1nlem  12065  fsumabs  12182  iserabs  12192  isumlessdc  12213  divcnv  12214  expcnvre  12220  absgtap  12227  georeclim  12230  cvgratnnlembern  12240  cvgratnnlemsumlt  12245  cvgratnnlemfm  12246  cvgratnnlemrate  12247  mertenslemub  12251  mertenslemi1  12252  prodfclim1  12261  prodfap0  12262  efcvgfsum  12384  eftlub  12407  eflegeo  12418  tanval3ap  12431  tannegap  12445  ef01bndlem  12473  sin01bnd  12474  cos01bnd  12475  cos01gt0  12480  bitsfzolem  12671  bitsfzo  12672  bitsinv1lem  12678  mulgcd  12743  nnminle  12762  eucalglt  12785  lcmledvds  12798  mulgcddvds  12822  prmind2  12848  isprm5lem  12869  pw2dvdslemn  12893  pw2dvdseulemle  12895  oddpwdclemdvds  12898  sqrt2irrap  12908  divdenle  12925  nonsq  12935  pythagtriplem4  12997  pclem0  13015  pcpremul  13022  pczdvds  13043  pcprmpw2  13062  qexpz  13081  4sqlem10  13116  ballotfilemimin  13199  ballotfilemsel1i  13206  ballotfilemro  13216  ennnfonelemkh  13253  triv1nsgd  13970  qusgrp  13984  gzsumsplit0  14097  prdsbaslemss  14123  bl2in  15399  xblcntrps  15409  xblcntr  15410  ssblps  15421  ssbl  15422  blssps  15423  blss  15424  xmetxp  15503  mulc1cncf  15585  cncfmptc  15592  mulcncflem  15603  ivthinclemlopn  15632  ivthinclemuopn  15634  ivthdec  15640  ivthreinc  15641  hovera  15643  hoverlt1  15645  limcimolemlt  15660  cnplimclemle  15664  cnplimclemr  15665  limccnp2lem  15672  dveflem  15722  reeff1olem  15767  reeff1oleme  15768  tangtx  15834  cosq34lt1  15846  logdivlti  15877  cxpap0  15900  rpabscxpbnd  15936  pellexlem2  15977  mersenne  15996  lgslem3  16006  gausslemma2dlem1a  16062  lgsquadlem1  16081  lgsquadlem2  16082  2lgslem1c  16094  subumgredg2en  16397  qdencn  16948  cvgcmp2nlemabs  16957  trilpolemclim  16961  trilpolemisumle  16963  trilpolemeq1  16965  apdifflemf  16971  apdifflemr  16972