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

Metamath Proof Explorer

Theorem dmopab3

Description: The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004)

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

Proof

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