Theorem 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 “ 𝐴 ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		dfima3	⊢ ( I “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) }
2		df-br	⊢ ( 𝑥 I 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ I )
3		vex	⊢ 𝑦 ∈ V
4	3	ideq	⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
5	2 4	bitr3i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ↔ 𝑥 = 𝑦 )
6	5	anbi1ci	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) ↔ ( 𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴 ) )
7	6	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴 ) )
8		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
9	8	equsexvw	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴 ) ↔ 𝑦 ∈ 𝐴 )
10	7 9	bitri	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) ↔ 𝑦 ∈ 𝐴 )
11	10	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) } = { 𝑦 ∣ 𝑦 ∈ 𝐴 }
12		abid2	⊢ { 𝑦 ∣ 𝑦 ∈ 𝐴 } = 𝐴
13	1 11 12	3eqtri	⊢ ( I “ 𝐴 ) = 𝐴