Metamath Proof Explorer

Theorem imadmrnOLD

Description: Obsolete version of imadmrn as of 27-Sep-2026. (Contributed by NM, 14-Aug-1994) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	imadmrnOLD	$⊢ A [dom A] = ran A$

Proof

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	3	pm4.71i	$⊢ ⟨x, y⟩ \in A \leftrightarrow (⟨x, y⟩ \in A \land x \in dom A)$
5		ancom	$⊢ (⟨x, y⟩ \in A \land x \in dom A) \leftrightarrow (x \in dom A \land ⟨x, y⟩ \in A)$
6	4 5	bitr2i	$⊢ (x \in dom A \land ⟨x, y⟩ \in A) \leftrightarrow ⟨x, y⟩ \in A$
7	6	exbii	$⊢ \exists x (x \in dom A \land ⟨x, y⟩ \in A) \leftrightarrow \exists x ⟨x, y⟩ \in A$
8	7	abbii	$⊢ \{y \| \exists x (x \in dom A \land ⟨x, y⟩ \in A)\} = \{y \| \exists x ⟨x, y⟩ \in A\}$
9		dfima3	$⊢ A [dom A] = \{y \| \exists x (x \in dom A \land ⟨x, y⟩ \in A)\}$
10		dfrn3	$⊢ ran A = \{y \| \exists x ⟨x, y⟩ \in A\}$
11	8 9 10	3eqtr4i	$⊢ A [dom A] = ran A$