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

Theorem eqbrtrrd 3952
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 2145 . 2  |-  ( ph  ->  B  =  A )
3 eqbrtrrd.2 . 2  |-  ( ph  ->  A R C )
42, 3eqbrtrd 3950 1  |-  ( ph  ->  B R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331   class class class wbr 3929
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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930
This theorem is referenced by:  dftpos4  6160  phpm  6759  unsnfidcex  6808  fisseneq  6820  f1finf1o  6835  prmuloclemcalc  7380  mullocprlem  7385  cauappcvgprlemladdfl  7470  caucvgprlemopl  7484  caucvgprprlemloccalc  7499  caucvgprprlemopl  7512  ltadd1sr  7591  suplocsrlem  7623  axarch  7706  axpre-suploclemres  7716  lemulge11  8631  mul2lt0llt0  9555  mul2lt0lgt0  9556  mul2lt0pn  9558  xaddge0  9668  modqmuladdim  10147  ltexp2a  10352  leexp2a  10353  nnlesq  10403  faclbnd6  10497  facavg  10499  fiprsshashgt1  10570  cvg1nlemcxze  10761  resqrexlemover  10789  resqrexlemlo  10792  resqrexlemnmsq  10796  resqrexlemnm  10797  leabs  10853  abs3dif  10884  abs2dif  10885  maxabslemlub  10986  maxltsup  10997  bdtri  11018  xrmaxiflemab  11023  xrbdtri  11052  recn2  11093  imcn2  11094  iserex  11115  summodclem2a  11157  fsumge1  11237  isumrpcl  11270  cvgratnnlemseq  11302  cvgratnnlemsumlt  11304  mertenslemi1  11311  prodmodclem2a  11352  ege2le3  11384  efgt1p2  11408  efgt1p  11409  tanval2ap  11426  tanval3ap  11427  cos12dec  11480  eirraplem  11489  divalglemnqt  11623  mulgcd  11710  dvdssqlem  11724  nn0seqcvgd  11728  mulgcddvds  11781  rpdvds  11786  pw2dvdseulemle  11851  sqrt2irraplemnn  11863  qden1elz  11889  phimullem  11907  hashgcdlem  11909  hashgcdeq  11910  ennnfonelemex  11933  lmcn2  12458  psmetge0  12509  xmetge0  12543  cnopnap  12772  suplociccex  12781  ivthinclemlopn  12792  ivthinclemuopn  12794  cnplimclemr  12816  limccnp2lem  12823  dveflem  12864  efltlemlt  12872  cosq23lt0  12930  coseq0q4123  12931  cosq34lt1  12947  logdivlti  12973  apdiff  13292  taupi  13295
  Copyright terms: Public domain W3C validator