Theorem dfrn7

Description: The range is equal to the image of any class including the domain. (Contributed by BJ, 27-Sep-2026)

	Ref	Expression
Assertion	dfrn7	⊢ ( dom 𝐴 ⊆ 𝐵 → ran 𝐴 = ( 𝐴 “ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	opeldm	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑥 ∈ dom 𝐴 )
4		ssel	⊢ ( dom 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ dom 𝐴 → 𝑥 ∈ 𝐵 ) )
5	3 4	syl5	⊢ ( dom 𝐴 ⊆ 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
6	5	pm4.71rd	⊢ ( dom 𝐴 ⊆ 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
7	6	exbidv	⊢ ( dom 𝐴 ⊆ 𝐵 → ( ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
8	7	abbidv	⊢ ( dom 𝐴 ⊆ 𝐵 → { 𝑦 ∣ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) } )
9		dfrn3	⊢ ran 𝐴 = { 𝑦 ∣ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 }
10		dfima3	⊢ ( 𝐴 “ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) }
11	8 9 10	3eqtr4g	⊢ ( dom 𝐴 ⊆ 𝐵 → ran 𝐴 = ( 𝐴 “ 𝐵 ) )