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

Theorem breqtrd 3788
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 3776 . 2 (𝜑 → (𝐴𝑅𝐵𝐴𝑅𝐶))
41, 3mpbid 135 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243   class class class wbr 3764
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-br 3765
This theorem is referenced by:  breqtrrd  3790  syl5breq  3799  tfrexlem  5948  phplem4  6318  phplem4on  6329  fidifsnen  6331  fisbth  6340  fin0  6342  fin0or  6343  ltsonq  6494  addlocprlemeqgt  6628  prmuloclemcalc  6661  mullocprlem  6666  addcanprlemu  6711  ltaprlem  6714  ltaprg  6715  prplnqu  6716  ltmprr  6738  cauappcvgprlemopl  6742  cauappcvgprlemloc  6748  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  cauappcvgprlem1  6755  caucvgprlemm  6764  caucvgprlemopl  6765  caucvgprlemloc  6771  caucvgprprlemloccalc  6780  caucvgprprlemopl  6793  recexgt0sr  6856  prsrpos  6867  caucvgsrlemoffgt1  6881  caucvgsr  6884  pitoregt0  6923  add20  7467  mullt0  7473  ltmul1a  7580  ltm1  7810  recgt0  7814  prodgt0gt0  7815  prodgt0  7816  prodge0  7818  lemul1a  7822  recp1lt1  7863  recreclt  7864  ledivp1  7867  ltaddrp2d  8655  fz01en  8915  fzonmapblen  9041  qbtwnrelemcalc  9108  flqaddz  9137  flhalf  9142  frecfzen2  9178  serile  9227  ltexp2a  9280  leexp2a  9281  exple1  9284  expubnd  9285  bernneq  9343  cvg1nlemcxze  9555  cvg1nlemres  9558  recvguniqlem  9566  resqrexlemover  9582  resqrexlemdec  9583  resqrexlemcalc2  9587  resqrexlemcalc3  9588  resqrexlemnm  9590  resqrexlemoverl  9593  ltabs  9657  abslt  9658  absle  9659  abstri  9674  climge0  9819  climaddc2  9824  nn0seqcvgd  9854
  Copyright terms: Public domain W3C validator