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

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

Proof of Theorem eqbrtrrd
StepHypRef Expression
1 eqbrtrrd.1 . . 3 (𝜑𝐴 = 𝐵)
21eqcomd 2061 . 2 (𝜑𝐵 = 𝐴)
3 eqbrtrrd.2 . 2 (𝜑𝐴𝑅𝐶)
42, 3eqbrtrd 3811 1 (𝜑𝐵𝑅𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259   class class class wbr 3791
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-un 2949  df-sn 3408  df-pr 3409  df-op 3411  df-br 3792
This theorem is referenced by:  dftpos4  5908  phpm  6357  prmuloclemcalc  6720  mullocprlem  6725  cauappcvgprlemladdfl  6810  caucvgprlemopl  6824  caucvgprprlemloccalc  6839  caucvgprprlemopl  6852  ltadd1sr  6918  axarch  7022  lemulge11  7906  modqmuladdim  9316  ltexp2a  9471  leexp2a  9472  nnlesq  9521  faclbnd6  9611  facavg  9613  cvg1nlemcxze  9808  resqrexlemover  9836  resqrexlemlo  9839  resqrexlemnmsq  9843  resqrexlemnm  9844  leabs  9900  abs3dif  9931  abs2dif  9932  recn2  10067  imcn2  10068  iiserex  10089  pw2dvdseulemle  10234  nn0seqcvgd  10242
  Copyright terms: Public domain W3C validator