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

Theorem eqbrtrrd 3959
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
Hypotheses
Ref Expression
eqbrtrrd.1 (𝜑𝐴 = 𝐵)
eqbrtrrd.2 (𝜑𝐴𝑅𝐶)
Assertion
Ref Expression
eqbrtrrd (𝜑𝐵𝑅𝐶)

Proof of Theorem eqbrtrrd
StepHypRef Expression
1 eqbrtrrd.1 . . 3 (𝜑𝐴 = 𝐵)
21eqcomd 2146 . 2 (𝜑𝐵 = 𝐴)
3 eqbrtrrd.2 . 2 (𝜑𝐴𝑅𝐶)
42, 3eqbrtrd 3957 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:  dftpos4  6167  phpm  6766  unsnfidcex  6815  fisseneq  6827  f1finf1o  6842  prmuloclemcalc  7396  mullocprlem  7401  cauappcvgprlemladdfl  7486  caucvgprlemopl  7500  caucvgprprlemloccalc  7515  caucvgprprlemopl  7528  ltadd1sr  7607  suplocsrlem  7639  axarch  7722  axpre-suploclemres  7732  lemulge11  8647  mul2lt0llt0  9577  mul2lt0lgt0  9578  mul2lt0pn  9580  xaddge0  9690  modqmuladdim  10170  ltexp2a  10375  leexp2a  10376  nnlesq  10426  faclbnd6  10521  facavg  10523  fiprsshashgt1  10594  cvg1nlemcxze  10785  resqrexlemover  10813  resqrexlemlo  10816  resqrexlemnmsq  10820  resqrexlemnm  10821  leabs  10877  abs3dif  10908  abs2dif  10909  maxabslemlub  11010  maxltsup  11021  bdtri  11042  xrmaxiflemab  11047  xrbdtri  11076  recn2  11117  imcn2  11118  iserex  11139  summodclem2a  11181  fsumge1  11261  isumrpcl  11294  cvgratnnlemseq  11326  cvgratnnlemsumlt  11328  mertenslemi1  11335  prodmodclem2a  11376  ege2le3  11412  efgt1p2  11436  efgt1p  11437  tanval2ap  11454  tanval3ap  11455  cos12dec  11508  eirraplem  11517  divalglemnqt  11651  mulgcd  11738  dvdssqlem  11752  nn0seqcvgd  11756  mulgcddvds  11809  rpdvds  11814  pw2dvdseulemle  11879  sqrt2irraplemnn  11891  qden1elz  11917  phimullem  11935  hashgcdlem  11937  hashgcdeq  11938  ennnfonelemex  11961  lmcn2  12486  psmetge0  12537  xmetge0  12571  cnopnap  12800  suplociccex  12809  ivthinclemlopn  12820  ivthinclemuopn  12822  cnplimclemr  12844  limccnp2lem  12851  dveflem  12893  efltlemlt  12901  cosq23lt0  12960  coseq0q4123  12961  cosq34lt1  12977  logdivlti  13008  apdiff  13414  taupi  13428
  Copyright terms: Public domain W3C validator