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

Theorem eqbrtrrd 4029
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 2183 . 2 (𝜑𝐵 = 𝐴)
3 eqbrtrrd.2 . 2 (𝜑𝐴𝑅𝐶)
42, 3eqbrtrd 4027 1 (𝜑𝐵𝑅𝐶)
Colors of variables: wff set class
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:  dftpos4  6266  phpm  6867  unsnfidcex  6921  fisseneq  6933  f1finf1o  6948  prmuloclemcalc  7566  mullocprlem  7571  cauappcvgprlemladdfl  7656  caucvgprlemopl  7670  caucvgprprlemloccalc  7685  caucvgprprlemopl  7698  ltadd1sr  7777  suplocsrlem  7809  axarch  7892  axpre-suploclemres  7902  lemulge11  8825  mul2lt0llt0  9763  mul2lt0lgt0  9764  mul2lt0pn  9766  xaddge0  9880  modqmuladdim  10369  ltexp2a  10574  leexp2a  10575  nnlesq  10626  faclbnd6  10726  facavg  10728  fiprsshashgt1  10799  cvg1nlemcxze  10993  resqrexlemover  11021  resqrexlemlo  11024  resqrexlemnmsq  11028  resqrexlemnm  11029  leabs  11085  abs3dif  11116  abs2dif  11117  maxabslemlub  11218  maxltsup  11229  bdtri  11250  xrmaxiflemab  11257  xrbdtri  11286  recn2  11327  imcn2  11328  iserex  11349  summodclem2a  11391  fsumge1  11471  isumrpcl  11504  cvgratnnlemseq  11536  cvgratnnlemsumlt  11538  mertenslemi1  11545  prodmodclem2a  11586  ege2le3  11681  efgt1p2  11705  efgt1p  11706  tanval2ap  11723  tanval3ap  11724  cos12dec  11777  eirraplem  11786  divalglemnqt  11927  mulgcd  12019  dvdssqlem  12033  nn0seqcvgd  12043  mulgcddvds  12096  rpdvds  12101  isprm5  12144  pw2dvdseulemle  12169  sqrt2irraplemnn  12181  qden1elz  12207  phimullem  12227  hashgcdlem  12240  hashgcdeq  12241  pceu  12297  pcdvdstr  12328  pockthg  12357  ennnfonelemex  12417  lmcn2  13819  psmetge0  13870  xmetge0  13904  cnopnap  14133  suplociccex  14142  ivthinclemlopn  14153  ivthinclemuopn  14155  cnplimclemr  14177  limccnp2lem  14184  dveflem  14226  efltlemlt  14234  cosq23lt0  14293  coseq0q4123  14294  cosq34lt1  14310  logdivlti  14341  lgsne0  14478  apdiff  14835  taupi  14860
  Copyright terms: Public domain W3C validator