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  8344  prodgt0  8574  div4p1lem1div2  8931  mul2lt0rgt0  9502  xleadd1a  9611  xltadd1  9614  xlt2add  9618  xposdif  9620  xlesubadd  9621  xleaddadd  9625  uzsubsubfz  9782  fzctr  9865  subfzo0  9974  exbtwnzlemstep  9980  exbtwnzlemex  9982  rebtwn2zlemstep  9985  rebtwn2z  9987  qbtwnxr  9990  ceilqge  10038  modqge0  10060  modqlt  10061  modqid  10077  m1modge3gt1  10099  modaddmodup  10115  addmodlteq  10126  ser3mono  10206  ser3ge0  10245  ser3le  10246  leexp1a  10303  sqgt0ap  10316  sqge0  10324  nnlesq  10351  expnbnd  10370  nn0opthlem2d  10422  facwordi  10441  filtinf  10493  hashunlem  10505  zfz1isolemiso  10537  cjmulge0  10616  resqrexlemover  10737  resqrexlemdec  10738  resqrexlemlo  10740  resqrexlemcalc3  10743  resqrexlemcvg  10746  resqrexlemoverl  10748  resqrexlemglsq  10749  resqrexlemga  10750  absge0  10787  amgm2  10845  maxle1  10938  bdtrilem  10965  xrmaxifle  10970  xrmaxiflemlub  10972  xrmaxiflemval  10974  xrmax1sup  10977  xrmaxltsup  10982  xrmaxadd  10985  xrbdtri  11000  reccn2ap  11037  climle  11058  climserle  11069  isumclim2  11146  isumclim3  11147  isumge0  11154  fsumlessfi  11184  expcnvap0  11226  expcnvre  11227  explecnv  11229  absltap  11233  cvgratnnlembern  11247  cvgratnnlemnexp  11248  cvgratnnlemmn  11249  cvgratnnlemabsle  11251  cvgratnnlemfm  11253  cvgratnnlemrate  11254  mertenslemi1  11259  mertenslem2  11260  efcvg  11286  ege2le3  11291  efaddlem  11294  eftlub  11310  effsumlt  11312  ef01bndlem  11377  sin02gt0  11384  eirrap  11396  iddvdsexp  11429  dvdsadd  11448  dvdsfac  11470  dvdsmod  11472  omoe  11505  divalglemnn  11527  divalglemnqt  11529  flodddiv4t2lthalf  11546  dvdslegcd  11565  dfgcd3  11610  dvdssqim  11624  dvdsmulgcd  11625  nn0seqcvgd  11634  dvdslcm  11662  lcmgcdlem  11670  mulgcddvds  11687  qredeq  11689  cncongr2  11697  sqnprm  11728  isprm6  11737  sqpweven  11764  znege1  11767  sqrt2irrap  11769  nonsq  11796  hashdvds  11808  ennnfonelemkh  11836  psmetxrge0  12412  isxmet2d  12428  mettri  12453  xmettri3  12454  mettri3  12455  xblss2ps  12484  blss2ps  12486  blss2  12487  blssps  12507  blss  12508  xmetxp  12587  ivthdec  12702  sin0pilem1  12773  sinq12gt0  12822  cvgcmp2nlemabs  13123  trilpolemclim  13125  trilpolemeq1  13129
  Copyright terms: Public domain W3C validator