Theorem eqbrtrd 4026

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

Syntax hints:   → wi 4   = wceq 1353   class class class wbr 4004

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005

This theorem is referenced by:  eqbrtrrd  4028  dif1en  6879  ccfunen  7263  prarloclemcalc  7501  ltexprlemopu  7602  recexprlemloc  7630  caucvgprprlemloccalc  7683  suplocsrlem  7807  axpre-suploclemres  7900  mulle0r  8901  lbinfle  8907  divge1  9723  xltnegi  9835  xleadd1a  9873  xltadd1  9876  xlt2add  9880  xposdif  9882  xleaddadd  9887  ubmelm1fzo  10226  qbtwnrelemcalc  10256  qbtwnxr  10258  ceiqm1l  10311  ceilqm1lt  10312  ceilqle  10314  modqlt  10333  modqeqmodmin  10394  addmodlteq  10398  exp3vallem  10521  bernneq  10641  nn0ltexp2  10689  faclbnd2  10722  resqrexlemdec  11020  resqrexlemcalc2  11024  resqrexlemglsq  11031  resqrexlemga  11032  abslt  11097  amgm2  11127  icodiamlt  11189  maxabsle  11213  maxltsup  11227  minmax  11238  min1inf  11240  min2inf  11241  bdtrilem  11247  xrmaxltsup  11266  xrmaxaddlem  11268  xrmaxadd  11269  xrminmax  11273  xrmin1inf  11275  xrmin2inf  11276  climconst  11298  serclim0  11313  mulcn2  11320  reccn2ap  11321  iserex  11347  climlec2  11349  iserge0  11351  climcau  11355  climcvg1nlem  11357  fsumabs  11473  iserabs  11483  isumlessdc  11504  divcnv  11505  expcnvre  11511  absgtap  11518  georeclim  11521  cvgratnnlembern  11531  cvgratnnlemsumlt  11536  cvgratnnlemfm  11537  cvgratnnlemrate  11538  mertenslemub  11542  mertenslemi1  11543  prodfclim1  11552  prodfap0  11553  efcvgfsum  11675  eftlub  11698  eflegeo  11709  tanval3ap  11722  tannegap  11736  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  cos01gt0  11770  zsupssdc  11955  mulgcd  12017  nnminle  12036  eucalglt  12057  lcmledvds  12070  mulgcddvds  12094  prmind2  12120  isprm5lem  12141  pw2dvdslemn  12165  pw2dvdseulemle  12167  oddpwdclemdvds  12170  sqrt2irrap  12180  divdenle  12197  nonsq  12207  pythagtriplem4  12268  pclem0  12286  pcpremul  12293  pczdvds  12313  pcprmpw2  12332  qexpz  12350  4sqlem10  12385  ennnfonelemkh  12413  triv1nsgd  13078  bl2in  13906  xblcntrps  13916  xblcntr  13917  ssblps  13928  ssbl  13929  blssps  13930  blss  13931  xmetxp  14010  mulc1cncf  14079  cncfmptc  14085  mulcncflem  14093  ivthinclemlopn  14117  ivthinclemuopn  14119  ivthdec  14125  limcimolemlt  14136  cnplimclemle  14140  cnplimclemr  14141  limccnp2lem  14148  dveflem  14190  reeff1olem  14195  reeff1oleme  14196  tangtx  14262  cosq34lt1  14274  logdivlti  14305  cxpap0  14328  rpabscxpbnd  14362  lgslem3  14406  qdencn  14778  cvgcmp2nlemabs  14783  trilpolemclim  14787  trilpolemisumle  14789  trilpolemeq1  14791  apdifflemf  14797  apdifflemr  14798