Theorem rnopab3

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

	Ref	Expression
Assertion	rnopab3	⊢ ( ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 𝜑 ↔ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-ral	⊢ ( ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 𝜑 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ∃ 𝑥 𝜑 ) )
2		pm4.71	⊢ ( ( 𝑦 ∈ 𝐴 → ∃ 𝑥 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ↔ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝜑 ) ) )
3	2	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ∃ 𝑥 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝜑 ) ) )
4		rnopab	⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) }
5		19.42v	⊢ ( ∃ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝜑 ) )
6	5	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝜑 ) }
7	4 6	eqtri	⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝜑 ) }
8	7	eqeq1i	⊢ ( ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } = 𝐴 ↔ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝜑 ) } = 𝐴 )
9		eqcom	⊢ ( 𝐴 = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝜑 ) } ↔ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝜑 ) } = 𝐴 )
10		eqabb	⊢ ( 𝐴 = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝜑 ) } ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝜑 ) ) )
11	8 9 10	3bitr2ri	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝜑 ) ) ↔ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } = 𝐴 )
12	1 3 11	3bitri	⊢ ( ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 𝜑 ↔ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } = 𝐴 )