This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } = 𝐴 )