This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-tr

Description: Define the transitive class predicate. Not to be confused with a transitive relation (see cotr ). Definition of Enderton p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 (which is suggestive of the word "transitive"), dftr2c , dftr3 , dftr4 , dftr5 , and (when A is a set) unisuc . The term "complete" is used instead of "transitive" in Definition 3 of Suppes p. 130. (Contributed by NM, 29-Aug-1993)

		Ref	Expression
	Assertion	df-tr	$⊢ Tr A \leftrightarrow ⋃ A \subseteq A$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$class A$
1	0	wtr	$wff Tr A$
2	0	cuni	$class ⋃ A$
3	2 0	wss	$wff ⋃ A \subseteq A$
4	1 3	wb	$wff (Tr A \leftrightarrow ⋃ A \subseteq A)$