Theorem bj-dfmpoa

Description: An equivalent definition of df-mpo . (Contributed by BJ, 30-Dec-2020)

	Ref	Expression
Assertion	bj-dfmpoa	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) }

Proof

Step	Hyp	Ref	Expression
1		df-mpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑡 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑡 = 𝐶 ) }
2		dfoprab2	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑡 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑡 = 𝐶 ) } = { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑡 = 𝐶 ) ) }
3		ancom	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑡 = 𝐶 ) ↔ ( 𝑡 = 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
4	3	anbi2i	⊢ ( ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑡 = 𝐶 ) ) ↔ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑡 = 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) )
5		anass	⊢ ( ( ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ↔ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑡 = 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) )
6		an13	⊢ ( ( ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ) ) )
7	4 5 6	3bitr2i	⊢ ( ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑡 = 𝐶 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ) ) )
8	7	exbii	⊢ ( ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑡 = 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ) ) )
9		df-rex	⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ) ) )
10		r19.42v	⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ) )
11	8 9 10	3bitr2i	⊢ ( ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑡 = 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ) )
12	11	exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑡 = 𝐶 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ) )
13		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ) )
14	12 13	bitr4i	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑡 = 𝐶 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) )
15	14	opabbii	⊢ { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑡 = 𝐶 ) ) } = { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) }
16	1 2 15	3eqtri	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑠 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) }