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

Metamath Proof Explorer

Definition df-trans

Description: Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012)

		Ref	Expression
	Assertion	df-trans	$⊢ 𝖳𝗋𝖺𝗇𝗌 = V ∖ ran ((E \circ E) ∖ E)$

Step	Hyp	Ref	Expression
0		ctrans	$class 𝖳𝗋𝖺𝗇𝗌$
1		cvv	$class V$
2		cep	$class E$
3	2 2	ccom	$class (E \circ E)$
4	3 2	cdif	$class ((E \circ E) ∖ E)$
5	4	crn	$class ran ((E \circ E) ∖ E)$
6	1 5	cdif	$class (V ∖ ran ((E \circ E) ∖ E))$
7	0 6	wceq	$wff 𝖳𝗋𝖺𝗇𝗌 = V ∖ ran ((E \circ E) ∖ E)$