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

Theorem breqtrrd 3960
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 2146 . 2 (𝜑𝐵 = 𝐶)
41, 3breqtrd 3958 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1332   class class class wbr 3933
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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2689  df-un 3076  df-sn 3534  df-pr 3535  df-op 3537  df-br 3934
This theorem is referenced by:  frirrg  4276  unsnfidcex  6812  unsnfidcel  6813  addlocprlemeq  7361  ltexprlemopl  7429  recexprlemloc  7459  cauappcvgprlemopl  7474  cauappcvgprlemladdfu  7482  cauappcvgprlem1  7487  caucvgprlemopl  7497  caucvgprlemladdfu  7505  caucvgprprlemopl  7525  caucvgprprlemexbt  7534  mulgt0sr  7606  archsr  7610  caucvgsrlemoffgt1  7627  suplocsrlemb  7634  suplocsrlem  7636  mulap0r  8397  prodgt0  8630  div4p1lem1div2  8993  mul2lt0rgt0  9573  xleadd1a  9682  xltadd1  9685  xlt2add  9689  xposdif  9691  xlesubadd  9692  xleaddadd  9696  uzsubsubfz  9854  fzctr  9937  subfzo0  10046  exbtwnzlemstep  10052  exbtwnzlemex  10054  rebtwn2zlemstep  10057  rebtwn2z  10059  qbtwnxr  10062  ceilqge  10110  modqge0  10132  modqlt  10133  modqid  10149  m1modge3gt1  10171  modaddmodup  10187  addmodlteq  10198  ser3mono  10278  ser3ge0  10317  ser3le  10318  leexp1a  10375  sqgt0ap  10388  sqge0  10396  nnlesq  10423  expnbnd  10442  nn0opthlem2d  10495  facwordi  10514  filtinf  10566  hashunlem  10578  zfz1isolemiso  10610  cjmulge0  10689  resqrexlemover  10810  resqrexlemdec  10811  resqrexlemlo  10813  resqrexlemcalc3  10816  resqrexlemcvg  10819  resqrexlemoverl  10821  resqrexlemglsq  10822  resqrexlemga  10823  absge0  10860  amgm2  10918  maxle1  11011  bdtrilem  11038  xrmaxifle  11043  xrmaxiflemlub  11045  xrmaxiflemval  11047  xrmax1sup  11050  xrmaxltsup  11055  xrmaxadd  11058  xrbdtri  11073  reccn2ap  11110  climle  11131  climserle  11142  isumclim2  11219  isumclim3  11220  isumge0  11227  fsumlessfi  11257  expcnvap0  11299  expcnvre  11300  explecnv  11302  absltap  11306  cvgratnnlembern  11320  cvgratnnlemnexp  11321  cvgratnnlemmn  11322  cvgratnnlemabsle  11324  cvgratnnlemfm  11326  cvgratnnlemrate  11327  mertenslemi1  11332  mertenslem2  11333  clim2divap  11337  prodmodclem3  11372  efcvg  11400  ege2le3  11405  efaddlem  11408  eftlub  11424  effsumlt  11426  ef01bndlem  11490  sin02gt0  11497  eirrap  11511  iddvdsexp  11544  dvdsadd  11563  dvdsfac  11585  dvdsmod  11587  omoe  11620  divalglemnn  11642  divalglemnqt  11644  flodddiv4t2lthalf  11661  dvdslegcd  11680  dfgcd3  11725  dvdssqim  11739  dvdsmulgcd  11740  nn0seqcvgd  11749  dvdslcm  11777  lcmgcdlem  11785  mulgcddvds  11802  qredeq  11804  cncongr2  11812  sqnprm  11843  isprm6  11852  sqpweven  11880  znege1  11883  sqrt2irrap  11885  nonsq  11912  hashdvds  11924  ennnfonelemkh  11952  psmetxrge0  12531  isxmet2d  12547  mettri  12572  xmettri3  12573  mettri3  12574  xblss2ps  12603  blss2ps  12605  blss2  12606  blssps  12626  blss  12627  xmetxp  12706  ivthdec  12821  sin0pilem1  12901  sinq12gt0  12950  tangtx  12958  cosordlem  12969  cosq34lt1  12970  logdivlti  13001  logbgcd1irrap  13086  cvgcmp2nlemabs  13385  trilpolemclim  13387  trilpolemeq1  13391  apdifflemf  13397  apdifflemr  13398
  Copyright terms: Public domain W3C validator