Theorem eqbrtrd 4104

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 4092	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 167	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:  eqbrtrrd  4106  dif1en  7037  ccfunen  7446  prarloclemcalc  7685  ltexprlemopu  7786  recexprlemloc  7814  caucvgprprlemloccalc  7867  suplocsrlem  7991  axpre-suploclemres  8084  mulle0r  9087  lbinfle  9093  divge1  9915  xltnegi  10027  xleadd1a  10065  xltadd1  10068  xlt2add  10072  xposdif  10074  xleaddadd  10079  ubmelm1fzo  10427  zsupssdc  10453  qbtwnrelemcalc  10470  qbtwnxr  10472  ceiqm1l  10528  ceilqm1lt  10529  ceilqle  10531  modqlt  10550  modqeqmodmin  10611  addmodlteq  10615  seqf1oglem1  10736  exp3vallem  10757  bernneq  10877  nn0ltexp2  10926  faclbnd2  10959  ccatsymb  11132  ccatrn  11139  resqrexlemdec  11517  resqrexlemcalc2  11521  resqrexlemglsq  11528  resqrexlemga  11529  abslt  11594  amgm2  11624  icodiamlt  11686  maxabsle  11710  maxltsup  11724  minmax  11736  min1inf  11738  min2inf  11739  bdtrilem  11745  xrmaxltsup  11764  xrmaxaddlem  11766  xrmaxadd  11767  xrminmax  11771  xrmin1inf  11773  xrmin2inf  11774  climconst  11796  serclim0  11811  mulcn2  11818  reccn2ap  11819  iserex  11845  climlec2  11847  iserge0  11849  climcau  11853  climcvg1nlem  11855  fsumabs  11971  iserabs  11981  isumlessdc  12002  divcnv  12003  expcnvre  12009  absgtap  12016  georeclim  12019  cvgratnnlembern  12029  cvgratnnlemsumlt  12034  cvgratnnlemfm  12035  cvgratnnlemrate  12036  mertenslemub  12040  mertenslemi1  12041  prodfclim1  12050  prodfap0  12051  efcvgfsum  12173  eftlub  12196  eflegeo  12207  tanval3ap  12220  tannegap  12234  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  cos01gt0  12269  bitsfzolem  12460  bitsfzo  12461  bitsinv1lem  12467  mulgcd  12532  nnminle  12551  eucalglt  12574  lcmledvds  12587  mulgcddvds  12611  prmind2  12637  isprm5lem  12658  pw2dvdslemn  12682  pw2dvdseulemle  12684  oddpwdclemdvds  12687  sqrt2irrap  12697  divdenle  12714  nonsq  12724  pythagtriplem4  12786  pclem0  12804  pcpremul  12811  pczdvds  12832  pcprmpw2  12851  qexpz  12870  4sqlem10  12905  ennnfonelemkh  12978  prdsbaslemss  13302  triv1nsgd  13750  qusgrp  13764  bl2in  15071  xblcntrps  15081  xblcntr  15082  ssblps  15093  ssbl  15094  blssps  15095  blss  15096  xmetxp  15175  mulc1cncf  15257  cncfmptc  15264  mulcncflem  15275  ivthinclemlopn  15304  ivthinclemuopn  15306  ivthdec  15312  ivthreinc  15313  hovera  15315  hoverlt1  15317  limcimolemlt  15332  cnplimclemle  15336  cnplimclemr  15337  limccnp2lem  15344  dveflem  15394  reeff1olem  15439  reeff1oleme  15440  tangtx  15506  cosq34lt1  15518  logdivlti  15549  cxpap0  15572  rpabscxpbnd  15608  mersenne  15665  lgslem3  15675  gausslemma2dlem1a  15731  lgsquadlem1  15750  lgsquadlem2  15751  2lgslem1c  15763  qdencn  16354  cvgcmp2nlemabs  16359  trilpolemclim  16363  trilpolemisumle  16365  trilpolemeq1  16367  apdifflemf  16373  apdifflemr  16374