ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqbrtrd GIF version

Theorem eqbrtrd 3957
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
StepHypRef Expression
1 eqbrtrd.2 . 2 (𝜑𝐵𝑅𝐶)
2 eqbrtrd.1 . . 3 (𝜑𝐴 = 𝐵)
32breq1d 3946 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
41, 3mpbird 166 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1332   class class class wbr 3936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3079  df-sn 3537  df-pr 3538  df-op 3540  df-br 3937
This theorem is referenced by:  eqbrtrrd  3959  dif1en  6780  ccfunen  7095  prarloclemcalc  7333  ltexprlemopu  7434  recexprlemloc  7462  caucvgprprlemloccalc  7515  suplocsrlem  7639  axpre-suploclemres  7732  mulle0r  8725  lbinfle  8731  divge1  9539  xltnegi  9647  xleadd1a  9685  xltadd1  9688  xlt2add  9692  xposdif  9694  xleaddadd  9699  ubmelm1fzo  10033  qbtwnrelemcalc  10063  qbtwnxr  10065  ceiqm1l  10114  ceilqm1lt  10115  ceilqle  10117  modqlt  10136  modqeqmodmin  10197  addmodlteq  10201  exp3vallem  10324  bernneq  10442  faclbnd2  10519  resqrexlemdec  10814  resqrexlemcalc2  10818  resqrexlemglsq  10825  resqrexlemga  10826  abslt  10891  amgm2  10921  icodiamlt  10983  maxabsle  11007  maxltsup  11021  minmax  11032  min1inf  11034  min2inf  11035  bdtrilem  11041  xrmaxltsup  11058  xrmaxaddlem  11060  xrmaxadd  11061  xrminmax  11065  xrmin1inf  11067  xrmin2inf  11068  climconst  11090  serclim0  11105  mulcn2  11112  reccn2ap  11113  iserex  11139  climlec2  11141  iserge0  11143  climcau  11147  climcvg1nlem  11149  fsumabs  11265  iserabs  11275  isumlessdc  11296  divcnv  11297  expcnvre  11303  absgtap  11310  georeclim  11313  cvgratnnlembern  11323  cvgratnnlemsumlt  11328  cvgratnnlemfm  11329  cvgratnnlemrate  11330  mertenslemub  11334  mertenslemi1  11335  prodfclim1  11344  prodfap0  11345  efcvgfsum  11408  eftlub  11431  eflegeo  11442  tanval3ap  11455  tannegap  11469  ef01bndlem  11497  sin01bnd  11498  cos01bnd  11499  cos01gt0  11503  mulgcd  11738  eucalglt  11772  lcmledvds  11785  mulgcddvds  11809  prmind2  11835  pw2dvdslemn  11877  pw2dvdseulemle  11879  oddpwdclemdvds  11882  sqrt2irrap  11892  divdenle  11909  nonsq  11919  ennnfonelemkh  11959  bl2in  12609  xblcntrps  12619  xblcntr  12620  ssblps  12631  ssbl  12632  blssps  12633  blss  12634  xmetxp  12713  mulc1cncf  12782  cncfmptc  12788  mulcncflem  12796  ivthinclemlopn  12820  ivthinclemuopn  12822  ivthdec  12828  limcimolemlt  12839  cnplimclemle  12843  cnplimclemr  12844  limccnp2lem  12851  dveflem  12893  reeff1olem  12898  reeff1oleme  12899  tangtx  12965  cosq34lt1  12977  logdivlti  13008  cxpap0  13031  rpabscxpbnd  13065  qdencn  13395  cvgcmp2nlemabs  13400  trilpolemclim  13402  trilpolemisumle  13404  trilpolemeq1  13406  apdifflemf  13412  apdifflemr  13413
  Copyright terms: Public domain W3C validator