Theorem eqbrtrd 4027

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

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

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 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-br 4006

This theorem is referenced by:  eqbrtrrd  4029  dif1en  6881  ccfunen  7265  prarloclemcalc  7503  ltexprlemopu  7604  recexprlemloc  7632  caucvgprprlemloccalc  7685  suplocsrlem  7809  axpre-suploclemres  7902  mulle0r  8903  lbinfle  8909  divge1  9725  xltnegi  9837  xleadd1a  9875  xltadd1  9878  xlt2add  9882  xposdif  9884  xleaddadd  9889  ubmelm1fzo  10228  qbtwnrelemcalc  10258  qbtwnxr  10260  ceiqm1l  10313  ceilqm1lt  10314  ceilqle  10316  modqlt  10335  modqeqmodmin  10396  addmodlteq  10400  exp3vallem  10523  bernneq  10643  nn0ltexp2  10691  faclbnd2  10724  resqrexlemdec  11022  resqrexlemcalc2  11026  resqrexlemglsq  11033  resqrexlemga  11034  abslt  11099  amgm2  11129  icodiamlt  11191  maxabsle  11215  maxltsup  11229  minmax  11240  min1inf  11242  min2inf  11243  bdtrilem  11249  xrmaxltsup  11268  xrmaxaddlem  11270  xrmaxadd  11271  xrminmax  11275  xrmin1inf  11277  xrmin2inf  11278  climconst  11300  serclim0  11315  mulcn2  11322  reccn2ap  11323  iserex  11349  climlec2  11351  iserge0  11353  climcau  11357  climcvg1nlem  11359  fsumabs  11475  iserabs  11485  isumlessdc  11506  divcnv  11507  expcnvre  11513  absgtap  11520  georeclim  11523  cvgratnnlembern  11533  cvgratnnlemsumlt  11538  cvgratnnlemfm  11539  cvgratnnlemrate  11540  mertenslemub  11544  mertenslemi1  11545  prodfclim1  11554  prodfap0  11555  efcvgfsum  11677  eftlub  11700  eflegeo  11711  tanval3ap  11724  tannegap  11738  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  cos01gt0  11772  zsupssdc  11957  mulgcd  12019  nnminle  12038  eucalglt  12059  lcmledvds  12072  mulgcddvds  12096  prmind2  12122  isprm5lem  12143  pw2dvdslemn  12167  pw2dvdseulemle  12169  oddpwdclemdvds  12172  sqrt2irrap  12182  divdenle  12199  nonsq  12209  pythagtriplem4  12270  pclem0  12288  pcpremul  12295  pczdvds  12315  pcprmpw2  12334  qexpz  12352  4sqlem10  12387  ennnfonelemkh  12415  triv1nsgd  13083  bl2in  13942  xblcntrps  13952  xblcntr  13953  ssblps  13964  ssbl  13965  blssps  13966  blss  13967  xmetxp  14046  mulc1cncf  14115  cncfmptc  14121  mulcncflem  14129  ivthinclemlopn  14153  ivthinclemuopn  14155  ivthdec  14161  limcimolemlt  14172  cnplimclemle  14176  cnplimclemr  14177  limccnp2lem  14184  dveflem  14226  reeff1olem  14231  reeff1oleme  14232  tangtx  14298  cosq34lt1  14310  logdivlti  14341  cxpap0  14364  rpabscxpbnd  14398  lgslem3  14442  qdencn  14814  cvgcmp2nlemabs  14819  trilpolemclim  14823  trilpolemisumle  14825  trilpolemeq1  14827  apdifflemf  14833  apdifflemr  14834