cptdfc - Mathbox for Andrew Salmon

	Mathbox for Andrew Salmon		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cptdfc		Structured version Visualization version GIF version

Syntax Definition cptdfc 42078

Description: PtDf is a predicate that is crucial for the definition of lines as well as proving a number of important theorems.

**Hypotheses**
Ref	Expression
cA	class 𝐴
cB	class 𝐵

**Assertion**
Ref	Expression
cptdfc	class PtDf(𝐴, 𝐵)

See definition df-ptdf 42094 for more information.

Colors of variables: wff setvar class