Theorem rnopabss

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

	Ref	Expression
Assertion	rnopabss	⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		rnopab	⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) }
2		19.42v	⊢ ( ∃ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝜑 ) )
3	2	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝜑 ) }
4		ssab2	⊢ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝜑 ) } ⊆ 𝐴
5	3 4	eqsstri	⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴
6	1 5	eqsstri	⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴