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

Theorem eqbrtrrd 4054
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
Hypotheses
Ref Expression
eqbrtrrd.1  |-  ( ph  ->  A  =  B )
eqbrtrrd.2  |-  ( ph  ->  A R C )
Assertion
Ref Expression
eqbrtrrd  |-  ( ph  ->  B R C )

Proof of Theorem eqbrtrrd
StepHypRef Expression
1 eqbrtrrd.1 . . 3  |-  ( ph  ->  A  =  B )
21eqcomd 2199 . 2  |-  ( ph  ->  B  =  A )
3 eqbrtrrd.2 . 2  |-  ( ph  ->  A R C )
42, 3eqbrtrd 4052 1  |-  ( ph  ->  B R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1364   class class class wbr 4030
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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-br 4031
This theorem is referenced by:  dftpos4  6318  phpm  6923  unsnfidcex  6978  fisseneq  6990  f1finf1o  7008  prmuloclemcalc  7627  mullocprlem  7632  cauappcvgprlemladdfl  7717  caucvgprlemopl  7731  caucvgprprlemloccalc  7746  caucvgprprlemopl  7759  ltadd1sr  7838  suplocsrlem  7870  axarch  7953  axpre-suploclemres  7963  lemulge11  8887  mul2lt0llt0  9830  mul2lt0lgt0  9831  mul2lt0pn  9833  xaddge0  9947  modqmuladdim  10441  ltexp2a  10665  leexp2a  10666  nnlesq  10717  faclbnd6  10818  facavg  10820  fiprsshashgt1  10891  cvg1nlemcxze  11129  resqrexlemover  11157  resqrexlemlo  11160  resqrexlemnmsq  11164  resqrexlemnm  11165  leabs  11221  abs3dif  11252  abs2dif  11253  maxabslemlub  11354  maxltsup  11365  bdtri  11386  xrmaxiflemab  11393  xrbdtri  11422  recn2  11463  imcn2  11464  iserex  11485  summodclem2a  11527  fsumge1  11607  isumrpcl  11640  cvgratnnlemseq  11672  cvgratnnlemsumlt  11674  mertenslemi1  11681  prodmodclem2a  11722  ege2le3  11817  efgt1p2  11841  efgt1p  11842  tanval2ap  11859  tanval3ap  11860  cos12dec  11914  eirraplem  11923  divalglemnqt  12064  mulgcd  12156  dvdssqlem  12170  nn0seqcvgd  12182  mulgcddvds  12235  rpdvds  12240  isprm5  12283  pw2dvdseulemle  12308  sqrt2irraplemnn  12320  qden1elz  12346  phimullem  12366  hashgcdlem  12379  hashgcdeq  12380  pceu  12436  pcdvdstr  12468  pockthg  12498  4sqlem11  12542  ennnfonelemex  12574  znrrg  14159  lmcn2  14459  psmetge0  14510  xmetge0  14544  cnopnap  14790  suplociccex  14804  ivthinclemlopn  14815  ivthinclemuopn  14817  hoverb  14827  ivthdichlem  14830  cnplimclemr  14848  limccnp2lem  14855  dveflem  14905  efltlemlt  14950  cosq23lt0  15009  coseq0q4123  15010  cosq34lt1  15026  logdivlti  15057  lgsne0  15195  lgsquadlem1  15234  lgsquadlem2  15235  apdiff  15608  taupi  15633
  Copyright terms: Public domain W3C validator