Theorem dfmpt3

Description: Alternate definition for the maps-to notation df-mpt . (Contributed by Mario Carneiro, 30-Dec-2016)

	Ref	Expression
Assertion	dfmpt3	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
2		velsn	⊢ ( 𝑦 ∈ { 𝐵 } ↔ 𝑦 = 𝐵 )
3	2	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝐵 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) )
4	3	anbi2i	⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝐵 } ) ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) )
5	4	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝐵 } ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) )
6		eliunxp	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝐵 } ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝐵 } ) ) )
7		elopab	⊢ ( 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) )
8	5 6 7	3bitr4i	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝐵 } ) ↔ 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } )
9	8	eqriv	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝐵 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
10	1 9	eqtr4i	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝐵 } )