dfid7

Description: Definition of identity relation as the trivial closure. (Contributed by RP, 26-Jul-2020)

		Ref	Expression
	Assertion	dfid7	$⊢ I = (x \in V ⟼ ⋂ \{y \| (x \subseteq y \land ⊤)\})$

Step	Hyp	Ref	Expression
1		dfid4	$⊢ I = (x \in V ⟼ x)$
2		ancom	$⊢ (x \subseteq y \land ⊤) \leftrightarrow (⊤ \land x \subseteq y)$
3		truan	$⊢ (⊤ \land x \subseteq y) \leftrightarrow x \subseteq y$
4	2 3	bitri	$⊢ (x \subseteq y \land ⊤) \leftrightarrow x \subseteq y$
5	4	abbii	$⊢ \{y \| (x \subseteq y \land ⊤)\} = \{y \| x \subseteq y\}$
6	5	inteqi	$⊢ ⋂ \{y \| (x \subseteq y \land ⊤)\} = ⋂ \{y \| x \subseteq y\}$
7		vex	$⊢ x \in V$
8	7	intmin2	$⊢ ⋂ \{y \| x \subseteq y\} = x$
9	6 8	eqtri	$⊢ ⋂ \{y \| (x \subseteq y \land ⊤)\} = x$
10	9	mpteq2i	$⊢ (x \in V ⟼ ⋂ \{y \| (x \subseteq y \land ⊤)\}) = (x \in V ⟼ x)$
11	1 10	eqtr4i	$⊢ I = (x \in V ⟼ ⋂ \{y \| (x \subseteq y \land ⊤)\})$

Metamath Proof Explorer