Theorem eqbrtrd 4073

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 4061	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 167	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1373   class class class wbr 4051

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-br 4052

This theorem is referenced by:  eqbrtrrd  4075  dif1en  6991  ccfunen  7396  prarloclemcalc  7635  ltexprlemopu  7736  recexprlemloc  7764  caucvgprprlemloccalc  7817  suplocsrlem  7941  axpre-suploclemres  8034  mulle0r  9037  lbinfle  9043  divge1  9865  xltnegi  9977  xleadd1a  10015  xltadd1  10018  xlt2add  10022  xposdif  10024  xleaddadd  10029  ubmelm1fzo  10377  zsupssdc  10403  qbtwnrelemcalc  10420  qbtwnxr  10422  ceiqm1l  10478  ceilqm1lt  10479  ceilqle  10481  modqlt  10500  modqeqmodmin  10561  addmodlteq  10565  seqf1oglem1  10686  exp3vallem  10707  bernneq  10827  nn0ltexp2  10876  faclbnd2  10909  ccatsymb  11081  ccatrn  11088  resqrexlemdec  11397  resqrexlemcalc2  11401  resqrexlemglsq  11408  resqrexlemga  11409  abslt  11474  amgm2  11504  icodiamlt  11566  maxabsle  11590  maxltsup  11604  minmax  11616  min1inf  11618  min2inf  11619  bdtrilem  11625  xrmaxltsup  11644  xrmaxaddlem  11646  xrmaxadd  11647  xrminmax  11651  xrmin1inf  11653  xrmin2inf  11654  climconst  11676  serclim0  11691  mulcn2  11698  reccn2ap  11699  iserex  11725  climlec2  11727  iserge0  11729  climcau  11733  climcvg1nlem  11735  fsumabs  11851  iserabs  11861  isumlessdc  11882  divcnv  11883  expcnvre  11889  absgtap  11896  georeclim  11899  cvgratnnlembern  11909  cvgratnnlemsumlt  11914  cvgratnnlemfm  11915  cvgratnnlemrate  11916  mertenslemub  11920  mertenslemi1  11921  prodfclim1  11930  prodfap0  11931  efcvgfsum  12053  eftlub  12076  eflegeo  12087  tanval3ap  12100  tannegap  12114  ef01bndlem  12142  sin01bnd  12143  cos01bnd  12144  cos01gt0  12149  bitsfzolem  12340  bitsfzo  12341  bitsinv1lem  12347  mulgcd  12412  nnminle  12431  eucalglt  12454  lcmledvds  12467  mulgcddvds  12491  prmind2  12517  isprm5lem  12538  pw2dvdslemn  12562  pw2dvdseulemle  12564  oddpwdclemdvds  12567  sqrt2irrap  12577  divdenle  12594  nonsq  12604  pythagtriplem4  12666  pclem0  12684  pcpremul  12691  pczdvds  12712  pcprmpw2  12731  qexpz  12750  4sqlem10  12785  ennnfonelemkh  12858  prdsbaslemss  13181  triv1nsgd  13629  qusgrp  13643  bl2in  14950  xblcntrps  14960  xblcntr  14961  ssblps  14972  ssbl  14973  blssps  14974  blss  14975  xmetxp  15054  mulc1cncf  15136  cncfmptc  15143  mulcncflem  15154  ivthinclemlopn  15183  ivthinclemuopn  15185  ivthdec  15191  ivthreinc  15192  hovera  15194  hoverlt1  15196  limcimolemlt  15211  cnplimclemle  15215  cnplimclemr  15216  limccnp2lem  15223  dveflem  15273  reeff1olem  15318  reeff1oleme  15319  tangtx  15385  cosq34lt1  15397  logdivlti  15428  cxpap0  15451  rpabscxpbnd  15487  mersenne  15544  lgslem3  15554  gausslemma2dlem1a  15610  lgsquadlem1  15629  lgsquadlem2  15630  2lgslem1c  15642  qdencn  16107  cvgcmp2nlemabs  16112  trilpolemclim  16116  trilpolemisumle  16118  trilpolemeq1  16120  apdifflemf  16126  apdifflemr  16127