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 A \subseteq B \to ran A = A [B]$

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		vex	$⊢ y \in V$
3	1 2	opeldm	$⊢ ⟨x, y⟩ \in A \to x \in dom A$
4		ssel	$⊢ dom A \subseteq B \to (x \in dom A \to x \in B)$
5	3 4	syl5	$⊢ dom A \subseteq B \to (⟨x, y⟩ \in A \to x \in B)$
6	5	pm4.71rd	$⊢ dom A \subseteq B \to (⟨x, y⟩ \in A \leftrightarrow (x \in B \land ⟨x, y⟩ \in A))$
7	6	exbidv	$⊢ dom A \subseteq B \to (\exists x ⟨x, y⟩ \in A \leftrightarrow \exists x (x \in B \land ⟨x, y⟩ \in A))$
8	7	abbidv	$⊢ dom A \subseteq B \to \{y \| \exists x ⟨x, y⟩ \in A\} = \{y \| \exists x (x \in B \land ⟨x, y⟩ \in A)\}$
9		dfrn3	$⊢ ran A = \{y \| \exists x ⟨x, y⟩ \in A\}$
10		dfima3	$⊢ A [B] = \{y \| \exists x (x \in B \land ⟨x, y⟩ \in A)\}$
11	8 9 10	3eqtr4g	$⊢ dom A \subseteq B \to ran A = A [B]$

Metamath Proof Explorer