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		abeq2	⊢ ( 𝐴 = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝜑 ) } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝜑 ) ) )
11	8 9 10	3bitr2ri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝜑 ) ) ↔ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = 𝐴 )
12	1 3 11	3bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 ↔ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = 𝐴 )