imai

Description: Image under the identity relation. Theorem 3.16(viii) of Monk1 p. 38. (Contributed by NM, 30-Apr-1998)

		Ref	Expression
	Assertion	imai	$⊢ I [A] = A$

Step	Hyp	Ref	Expression
1		dfima3	$⊢ I [A] = \{y \| \exists x (x \in A \land ⟨x, y⟩ \in I)\}$
2		df-br	$⊢ x I y \leftrightarrow ⟨x, y⟩ \in I$
3		vex	$⊢ y \in V$
4	3	ideq	$⊢ x I y \leftrightarrow x = y$
5	2 4	bitr3i	$⊢ ⟨x, y⟩ \in I \leftrightarrow x = y$
6	5	anbi1ci	$⊢ (x \in A \land ⟨x, y⟩ \in I) \leftrightarrow (x = y \land x \in A)$
7	6	exbii	$⊢ \exists x (x \in A \land ⟨x, y⟩ \in I) \leftrightarrow \exists x (x = y \land x \in A)$
8		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
9	8	equsexvw	$⊢ \exists x (x = y \land x \in A) \leftrightarrow y \in A$
10	7 9	bitri	$⊢ \exists x (x \in A \land ⟨x, y⟩ \in I) \leftrightarrow y \in A$
11	10	abbii	$⊢ \{y \| \exists x (x \in A \land ⟨x, y⟩ \in I)\} = \{y \| y \in A\}$
12		abid2	$⊢ \{y \| y \in A\} = A$
13	1 11 12	3eqtri	$⊢ I [A] = A$

Metamath Proof Explorer