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

Metamath Proof Explorer

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