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

Metamath Proof Explorer

Theorem dftr2

Description: An alternate way of defining a transitive class. Exercise 7 of TakeutiZaring p. 40. Using dftr2c instead may avoid dependences on ax-11 . (Contributed by NM, 24-Apr-1994)

		Ref	Expression
	Assertion	dftr2	$⊢ Tr A \leftrightarrow \forall x \forall y ((x \in y \land y \in A) \to x \in A)$

Proof

Step	Hyp	Ref	Expression
1		df-ss	$⊢ ⋃ A \subseteq A \leftrightarrow \forall x (x \in ⋃ A \to x \in A)$
2		df-tr	$⊢ Tr A \leftrightarrow ⋃ A \subseteq A$
3		19.23v	$⊢ \forall y ((x \in y \land y \in A) \to x \in A) \leftrightarrow (\exists y (x \in y \land y \in A) \to x \in A)$
4		eluni	$⊢ x \in ⋃ A \leftrightarrow \exists y (x \in y \land y \in A)$
5	4	imbi1i	$⊢ (x \in ⋃ A \to x \in A) \leftrightarrow (\exists y (x \in y \land y \in A) \to x \in A)$
6	3 5	bitr4i	$⊢ \forall y ((x \in y \land y \in A) \to x \in A) \leftrightarrow (x \in ⋃ A \to x \in A)$
7	6	albii	$⊢ \forall x \forall y ((x \in y \land y \in A) \to x \in A) \leftrightarrow \forall x (x \in ⋃ A \to x \in A)$
8	1 2 7	3bitr4i	$⊢ Tr A \leftrightarrow \forall x \forall y ((x \in y \land y \in A) \to x \in A)$