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