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

Metamath Proof Explorer

Theorem imadmrn

Description: The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994)

Ref Expression
Assertion imadmrn ( 𝐴 “ dom 𝐴 ) = ran 𝐴

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 vex ⊢ 𝑦 ∈ V
3 1 2 opeldm ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑥 ∈ dom 𝐴 )
4 3 pm4.71i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ∧ 𝑥 ∈ dom 𝐴 ) )
5 ancom ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ∧ 𝑥 ∈ dom 𝐴 ) ↔ ( 𝑥 ∈ dom 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
6 4 5 bitr2i ⊢ ( ( 𝑥 ∈ dom 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
7 6 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ dom 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ↔ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
8 7 abbii ⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ dom 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) } = { 𝑦 ∣ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 }
9 dfima3 ⊢ ( 𝐴 “ dom 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ dom 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) }
10 dfrn3 ⊢ ran 𝐴 = { 𝑦 ∣ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 }
11 8 9 10 3eqtr4i ⊢ ( 𝐴 “ dom 𝐴 ) = ran 𝐴