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

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

Proof of Theorem breqtrd
StepHypRef Expression
1 breqtrd.1 . 2 (𝜑𝐴𝑅𝐵)
2 breqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
32breq2d 3911 . 2 (𝜑 → (𝐴𝑅𝐵𝐴𝑅𝐶))
41, 3mpbid 146 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316   class class class wbr 3899
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-br 3900
This theorem is referenced by:  breqtrrd  3926  breqtrid  3935  tfrexlem  6199  phplem4  6717  phplem4on  6729  fidifsnen  6732  fisbth  6745  fin0  6747  fin0or  6748  ltsonq  7174  addlocprlemeqgt  7308  prmuloclemcalc  7341  mullocprlem  7346  addcanprlemu  7391  ltaprlem  7394  ltaprg  7395  prplnqu  7396  ltmprr  7418  cauappcvgprlemopl  7422  cauappcvgprlemloc  7428  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  cauappcvgprlem1  7435  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemloc  7451  caucvgprprlemloccalc  7460  caucvgprprlemopl  7473  recexgt0sr  7549  ltm1sr  7553  prsrpos  7561  caucvgsrlemoffgt1  7575  caucvgsr  7578  suplocsrlempr  7583  pitoregt0  7625  axpre-suploclemres  7677  add20  8204  mullt0  8210  ltmul1a  8321  ltm1  8572  recgt0  8576  prodgt0gt0  8577  prodgt0  8578  prodge0  8580  lemul1a  8584  recp1lt1  8625  recreclt  8626  ledivp1  8629  mulle0r  8670  ltaddrp2d  9486  mul2lt0np  9518  xleadd1a  9624  xleaddadd  9638  fz01en  9801  fzonmapblen  9932  qbtwnrelemcalc  10001  flqaddz  10038  flhalf  10043  flqdiv  10062  modqmuladdim  10108  modqsubdir  10134  addmodlteq  10139  frecfzen2  10168  iseqf1olemab  10230  ser3le  10259  ltexp2a  10313  leexp2a  10314  exple1  10317  expubnd  10318  bernneq  10380  faclbnd6  10458  hashfz  10535  zfz1isolemiso  10550  zfz1iso  10552  seq3coll  10553  cvg1nlemcxze  10722  cvg1nlemres  10725  recvguniqlem  10734  resqrexlemover  10750  resqrexlemdec  10751  resqrexlemcalc2  10755  resqrexlemcalc3  10756  resqrexlemnm  10758  resqrexlemoverl  10761  ltabs  10827  abslt  10828  absle  10829  abstri  10844  maxabslemlub  10947  maxabslemval  10948  dfabsmax  10957  bdtrilem  10978  xrmaxiflemab  10984  xrmaxiflemlub  10985  xrmaxaddlem  10997  reccn2ap  11050  climge0  11062  climaddc2  11067  summodclem2a  11118  zsumdc  11121  isumge0  11167  fsumle  11200  fsumlt  11201  isumshft  11227  expcnvap0  11239  geolim  11248  geolim2  11249  georeclim  11250  geo2lim  11253  cvgratnnlembern  11260  cvgratnnlemfm  11266  mertenslemi1  11272  mertensabs  11274  efcllemp  11291  ef0lem  11293  efgt0  11317  eftlub  11323  efltim  11331  sinbnd  11386  cosbnd  11387  ef01bndlem  11390  sin01gt0  11395  cos01gt0  11396  sin02gt0  11397  eirraplem  11410  dvdssub2  11462  dvdsadd2b  11467  dvdsexp  11486  opoe  11519  divalglemeunn  11545  divalglemex  11546  divalglemeuneg  11547  gcdaddm  11599  bezoutlemstep  11612  dvdsgcd  11627  dvdsmulgcd  11640  bezoutr1  11648  nn0seqcvgd  11649  rpmulgcd2  11703  qredeq  11704  rpdvds  11707  prmind2  11728  divdenle  11802  phicl2  11817  hashdvds  11824  phimullem  11828  ennnfonelemkh  11852  ennnfonelemnn0  11862  psmetsym  12425  psmettri  12426  mettri2  12458  xmetsym  12464  xmettri  12468  metrtri  12473  xblss2ps  12500  xblss2  12501  blhalf  12504  xmsge0  12563  cnmet  12626  ivthinclemlopn  12710  dveflem  12782  dvef  12783  sin0pilem1  12789  sinq12gt0  12838  sinq34lt0t  12839  cosq14gt0  12840  coseq0q4123  12842  pwf1oexmid  13121  qdencn  13149  cvgcmp2nlemabs  13154
  Copyright terms: Public domain W3C validator