Metamath Proof Explorer
Table of Contents - 20.33.2. Additional statements on relations and subclasses
- al3im
- intima0
- elimaint
- cnviun
- imaiun1
- coiun1
- elintima
- intimass
- intimass2
- intimag
- intimasn
- intimasn2
- ss2iundf
- ss2iundv
- cbviuneq12df
- cbviuneq12dv
- conrel1d
- conrel2d
- Transitive relations (not to be confused with transitive classes).
- trrelind
- xpintrreld
- restrreld
- trrelsuperreldg
- trficl
- cnvtrrel
- trrelsuperrel2dg
- Reflexive closures
- crcl
- df-rcl
- dfrcl2
- dfrcl3
- dfrcl4
- Finite relationship composition.
- relexp2
- relexpnul
- eliunov2
- eltrclrec
- elrtrclrec
- briunov2
- brmptiunrelexpd
- fvmptiunrelexplb0d
- fvmptiunrelexplb0da
- fvmptiunrelexplb1d
- brfvid
- brfvidRP
- fvilbd
- fvilbdRP
- brfvrcld
- brfvrcld2
- fvrcllb0d
- fvrcllb0da
- fvrcllb1d
- brtrclrec
- brrtrclrec
- briunov2uz
- eliunov2uz
- ov2ssiunov2
- relexp0eq
- iunrelexp0
- relexpxpnnidm
- relexpiidm
- relexpss1d
- comptiunov2i
- corclrcl
- iunrelexpmin1
- relexpmulnn
- relexpmulg
- trclrelexplem
- iunrelexpmin2
- relexp01min
- relexp1idm
- relexp0idm
- relexp0a
- relexpxpmin
- relexpaddss
- iunrelexpuztr
- Transitive closure of a relation
- dftrcl3
- brfvtrcld
- fvtrcllb1d
- trclfvcom
- cnvtrclfv
- cotrcltrcl
- trclimalb2
- brtrclfv2
- trclfvdecomr
- trclfvdecoml
- dmtrclfvRP
- rntrclfvRP
- rntrclfv
- dfrtrcl3
- brfvrtrcld
- fvrtrcllb0d
- fvrtrcllb0da
- fvrtrcllb1d
- dfrtrcl4
- corcltrcl
- cortrcltrcl
- corclrtrcl
- cotrclrcl
- cortrclrcl
- cotrclrtrcl
- cortrclrtrcl
- Adapted from Frege
- frege77d
- frege81d
- frege83d
- frege96d
- frege87d
- frege91d
- frege97d
- frege98d
- frege102d
- frege106d
- frege108d
- frege109d
- frege114d
- frege111d
- frege122d
- frege124d
- frege126d
- frege129d
- frege131d
- frege133d