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

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

Proof of Theorem breqtrrd
StepHypRef Expression
1 breqtrrd.1 . 2 (𝜑𝐴𝑅𝐵)
2 breqtrrd.2 . . 3 (𝜑𝐶 = 𝐵)
32eqcomd 2123 . 2 (𝜑𝐵 = 𝐶)
41, 3breqtrd 3924 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:  frirrg  4242  unsnfidcex  6776  unsnfidcel  6777  addlocprlemeq  7309  ltexprlemopl  7377  recexprlemloc  7407  cauappcvgprlemopl  7422  cauappcvgprlemladdfu  7430  cauappcvgprlem1  7435  caucvgprlemopl  7445  caucvgprlemladdfu  7453  caucvgprprlemopl  7473  caucvgprprlemexbt  7482  mulgt0sr  7554  archsr  7558  caucvgsrlemoffgt1  7575  suplocsrlemb  7582  suplocsrlem  7584  mulap0r  8345  prodgt0  8578  div4p1lem1div2  8941  mul2lt0rgt0  9515  xleadd1a  9624  xltadd1  9627  xlt2add  9631  xposdif  9633  xlesubadd  9634  xleaddadd  9638  uzsubsubfz  9795  fzctr  9878  subfzo0  9987  exbtwnzlemstep  9993  exbtwnzlemex  9995  rebtwn2zlemstep  9998  rebtwn2z  10000  qbtwnxr  10003  ceilqge  10051  modqge0  10073  modqlt  10074  modqid  10090  m1modge3gt1  10112  modaddmodup  10128  addmodlteq  10139  ser3mono  10219  ser3ge0  10258  ser3le  10259  leexp1a  10316  sqgt0ap  10329  sqge0  10337  nnlesq  10364  expnbnd  10383  nn0opthlem2d  10435  facwordi  10454  filtinf  10506  hashunlem  10518  zfz1isolemiso  10550  cjmulge0  10629  resqrexlemover  10750  resqrexlemdec  10751  resqrexlemlo  10753  resqrexlemcalc3  10756  resqrexlemcvg  10759  resqrexlemoverl  10761  resqrexlemglsq  10762  resqrexlemga  10763  absge0  10800  amgm2  10858  maxle1  10951  bdtrilem  10978  xrmaxifle  10983  xrmaxiflemlub  10985  xrmaxiflemval  10987  xrmax1sup  10990  xrmaxltsup  10995  xrmaxadd  10998  xrbdtri  11013  reccn2ap  11050  climle  11071  climserle  11082  isumclim2  11159  isumclim3  11160  isumge0  11167  fsumlessfi  11197  expcnvap0  11239  expcnvre  11240  explecnv  11242  absltap  11246  cvgratnnlembern  11260  cvgratnnlemnexp  11261  cvgratnnlemmn  11262  cvgratnnlemabsle  11264  cvgratnnlemfm  11266  cvgratnnlemrate  11267  mertenslemi1  11272  mertenslem2  11273  efcvg  11299  ege2le3  11304  efaddlem  11307  eftlub  11323  effsumlt  11325  ef01bndlem  11390  sin02gt0  11397  eirrap  11411  iddvdsexp  11444  dvdsadd  11463  dvdsfac  11485  dvdsmod  11487  omoe  11520  divalglemnn  11542  divalglemnqt  11544  flodddiv4t2lthalf  11561  dvdslegcd  11580  dfgcd3  11625  dvdssqim  11639  dvdsmulgcd  11640  nn0seqcvgd  11649  dvdslcm  11677  lcmgcdlem  11685  mulgcddvds  11702  qredeq  11704  cncongr2  11712  sqnprm  11743  isprm6  11752  sqpweven  11780  znege1  11783  sqrt2irrap  11785  nonsq  11812  hashdvds  11824  ennnfonelemkh  11852  psmetxrge0  12428  isxmet2d  12444  mettri  12469  xmettri3  12470  mettri3  12471  xblss2ps  12500  blss2ps  12502  blss2  12503  blssps  12523  blss  12524  xmetxp  12603  ivthdec  12718  sin0pilem1  12789  sinq12gt0  12838  tangtx  12846  cosordlem  12857  cosq34lt1  12858  cvgcmp2nlemabs  13154  trilpolemclim  13156  trilpolemeq1  13160
  Copyright terms: Public domain W3C validator