Metamath Proof Explorer


Table of Contents - 20.33.2. Additional statements on relations and subclasses

  1. al3im
  2. intima0
  3. elimaint
  4. cnviun
  5. imaiun1
  6. coiun1
  7. elintima
  8. intimass
  9. intimass2
  10. intimag
  11. intimasn
  12. intimasn2
  13. ss2iundf
  14. ss2iundv
  15. cbviuneq12df
  16. cbviuneq12dv
  17. conrel1d
  18. conrel2d
  19. Transitive relations (not to be confused with transitive classes).
    1. trrelind
    2. xpintrreld
    3. restrreld
    4. trrelsuperreldg
    5. trficl
    6. cnvtrrel
    7. trrelsuperrel2dg
  20. Reflexive closures
    1. crcl
    2. df-rcl
    3. dfrcl2
    4. dfrcl3
    5. dfrcl4
  21. Finite relationship composition.
    1. relexp2
    2. relexpnul
    3. eliunov2
    4. eltrclrec
    5. elrtrclrec
    6. briunov2
    7. brmptiunrelexpd
    8. fvmptiunrelexplb0d
    9. fvmptiunrelexplb0da
    10. fvmptiunrelexplb1d
    11. brfvid
    12. brfvidRP
    13. fvilbd
    14. fvilbdRP
    15. brfvrcld
    16. brfvrcld2
    17. fvrcllb0d
    18. fvrcllb0da
    19. fvrcllb1d
    20. brtrclrec
    21. brrtrclrec
    22. briunov2uz
    23. eliunov2uz
    24. ov2ssiunov2
    25. relexp0eq
    26. iunrelexp0
    27. relexpxpnnidm
    28. relexpiidm
    29. relexpss1d
    30. comptiunov2i
    31. corclrcl
    32. iunrelexpmin1
    33. relexpmulnn
    34. relexpmulg
    35. trclrelexplem
    36. iunrelexpmin2
    37. relexp01min
    38. relexp1idm
    39. relexp0idm
    40. relexp0a
    41. relexpxpmin
    42. relexpaddss
    43. iunrelexpuztr
  22. Transitive closure of a relation
    1. dftrcl3
    2. brfvtrcld
    3. fvtrcllb1d
    4. trclfvcom
    5. cnvtrclfv
    6. cotrcltrcl
    7. trclimalb2
    8. brtrclfv2
    9. trclfvdecomr
    10. trclfvdecoml
    11. dmtrclfvRP
    12. rntrclfvRP
    13. rntrclfv
    14. dfrtrcl3
    15. brfvrtrcld
    16. fvrtrcllb0d
    17. fvrtrcllb0da
    18. fvrtrcllb1d
    19. dfrtrcl4
    20. corcltrcl
    21. cortrcltrcl
    22. corclrtrcl
    23. cotrclrcl
    24. cortrclrcl
    25. cotrclrtrcl
    26. cortrclrtrcl
  23. Adapted from Frege
    1. frege77d
    2. frege81d
    3. frege83d
    4. frege96d
    5. frege87d
    6. frege91d
    7. frege97d
    8. frege98d
    9. frege102d
    10. frege106d
    11. frege108d
    12. frege109d
    13. frege114d
    14. frege111d
    15. frege122d
    16. frege124d
    17. frege126d
    18. frege129d
    19. frege131d
    20. frege133d