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 𝐴