rnopab3

Description: The range of a restricted class of ordered pairs. (Contributed by Eric Schmidt, 16-Sep-2025)

		Ref	Expression
	Assertion	rnopab3	$⊢ \forall y \in A \exists x φ \leftrightarrow ran \{⟨x, y⟩ \| (y \in A \land φ)\} = A$

Step	Hyp	Ref	Expression
1		df-ral	$⊢ \forall y \in A \exists x φ \leftrightarrow \forall y (y \in A \to \exists x φ)$
2		pm4.71	$⊢ (y \in A \to \exists x φ) \leftrightarrow (y \in A \leftrightarrow (y \in A \land \exists x φ))$
3	2	albii	$⊢ \forall y (y \in A \to \exists x φ) \leftrightarrow \forall y (y \in A \leftrightarrow (y \in A \land \exists x φ))$
4		rnopab	$⊢ ran \{⟨x, y⟩ \| (y \in A \land φ)\} = \{y \| \exists x (y \in A \land φ)\}$
5		19.42v	$⊢ \exists x (y \in A \land φ) \leftrightarrow (y \in A \land \exists x φ)$
6	5	abbii	$⊢ \{y \| \exists x (y \in A \land φ)\} = \{y \| (y \in A \land \exists x φ)\}$
7	4 6	eqtri	$⊢ ran \{⟨x, y⟩ \| (y \in A \land φ)\} = \{y \| (y \in A \land \exists x φ)\}$
8	7	eqeq1i	$⊢ ran \{⟨x, y⟩ \| (y \in A \land φ)\} = A \leftrightarrow \{y \| (y \in A \land \exists x φ)\} = A$
9		eqcom	$⊢ A = \{y \| (y \in A \land \exists x φ)\} \leftrightarrow \{y \| (y \in A \land \exists x φ)\} = A$
10		eqabb	$⊢ A = \{y \| (y \in A \land \exists x φ)\} \leftrightarrow \forall y (y \in A \leftrightarrow (y \in A \land \exists x φ))$
11	8 9 10	3bitr2ri	$⊢ \forall y (y \in A \leftrightarrow (y \in A \land \exists x φ)) \leftrightarrow ran \{⟨x, y⟩ \| (y \in A \land φ)\} = A$
12	1 3 11	3bitri	$⊢ \forall y \in A \exists x φ \leftrightarrow ran \{⟨x, y⟩ \| (y \in A \land φ)\} = A$

Metamath Proof Explorer