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

Metamath Proof Explorer

Theorem dftr2c

Description: Variant of dftr2 with commuted quantifiers, useful for shortening proofs and avoiding ax-11 . (Contributed by BTernaryTau, 28-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		dftr2	$⊢ Tr A \leftrightarrow \forall x \forall y ((x \in y \land y \in A) \to x \in A)$
2		elequ1	$⊢ x = z \to (x \in y \leftrightarrow z \in y)$
3	2	anbi1d	$⊢ x = z \to ((x \in y \land y \in A) \leftrightarrow (z \in y \land y \in A))$
4		eleq1w	$⊢ x = z \to (x \in A \leftrightarrow z \in A)$
5	3 4	imbi12d	$⊢ x = z \to (((x \in y \land y \in A) \to x \in A) \leftrightarrow ((z \in y \land y \in A) \to z \in A))$
6		elequ2	$⊢ y = z \to (x \in y \leftrightarrow x \in z)$
7		eleq1w	$⊢ y = z \to (y \in A \leftrightarrow z \in A)$
8	6 7	anbi12d	$⊢ y = z \to ((x \in y \land y \in A) \leftrightarrow (x \in z \land z \in A))$
9	8	imbi1d	$⊢ y = z \to (((x \in y \land y \in A) \to x \in A) \leftrightarrow ((x \in z \land z \in A) \to x \in A))$
10	5 9	alcomw	$⊢ \forall x \forall y ((x \in y \land y \in A) \to x \in A) \leftrightarrow \forall y \forall x ((x \in y \land y \in A) \to x \in A)$
11	1 10	bitri	$⊢ Tr A \leftrightarrow \forall y \forall x ((x \in y \land y \in A) \to x \in A)$