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

Metamath Proof Explorer

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 ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝐵 } )