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

Metamath Proof Explorer

Theorem elsnxp

Description: Membership in a Cartesian product with a singleton. (Contributed by Thierry Arnoux, 10-Apr-2020) (Proof shortened by JJ, 14-Jul-2021)

Ref Expression
Assertion elsnxp ( 𝑋 ∈ 𝑉 → ( 𝑍 ∈ ( { 𝑋 } × 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑍 = ⟨ 𝑋 , 𝑦 ⟩ ) )

Proof

Step Hyp Ref Expression
1 elxp ⊢ ( 𝑍 ∈ ( { 𝑋 } × 𝐴 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑍 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { 𝑋 } ∧ 𝑦 ∈ 𝐴 ) ) )
2 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ∈ { 𝑋 } ∧ 𝑍 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ { 𝑋 } ∧ 𝑍 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
3 an13 ⊢ ( ( 𝑍 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { 𝑋 } ∧ 𝑦 ∈ 𝐴 ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ { 𝑋 } ∧ 𝑍 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
4 3 exbii ⊢ ( ∃ 𝑦 ( 𝑍 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { 𝑋 } ∧ 𝑦 ∈ 𝐴 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ { 𝑋 } ∧ 𝑍 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
5 2 4 bitr4i ⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ∈ { 𝑋 } ∧ 𝑍 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∃ 𝑦 ( 𝑍 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { 𝑋 } ∧ 𝑦 ∈ 𝐴 ) ) )
6 elsni ⊢ ( 𝑥 ∈ { 𝑋 } → 𝑥 = 𝑋 )
7 6 opeq1d ⊢ ( 𝑥 ∈ { 𝑋 } → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑦 ⟩ )
8 7 eqeq2d ⊢ ( 𝑥 ∈ { 𝑋 } → ( 𝑍 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑍 = ⟨ 𝑋 , 𝑦 ⟩ ) )
9 8 biimpa ⊢ ( ( 𝑥 ∈ { 𝑋 } ∧ 𝑍 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑍 = ⟨ 𝑋 , 𝑦 ⟩ )
10 9 reximi ⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ∈ { 𝑋 } ∧ 𝑍 = ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑦 ∈ 𝐴 𝑍 = ⟨ 𝑋 , 𝑦 ⟩ )
11 5 10 sylbir ⊢ ( ∃ 𝑦 ( 𝑍 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { 𝑋 } ∧ 𝑦 ∈ 𝐴 ) ) → ∃ 𝑦 ∈ 𝐴 𝑍 = ⟨ 𝑋 , 𝑦 ⟩ )
12 11 exlimiv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑍 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { 𝑋 } ∧ 𝑦 ∈ 𝐴 ) ) → ∃ 𝑦 ∈ 𝐴 𝑍 = ⟨ 𝑋 , 𝑦 ⟩ )
13 1 12 sylbi ⊢ ( 𝑍 ∈ ( { 𝑋 } × 𝐴 ) → ∃ 𝑦 ∈ 𝐴 𝑍 = ⟨ 𝑋 , 𝑦 ⟩ )
14 snidg ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ { 𝑋 } )
15 opelxpi ⊢ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑦 ∈ 𝐴 ) → ⟨ 𝑋 , 𝑦 ⟩ ∈ ( { 𝑋 } × 𝐴 ) )
16 14 15 sylan ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴 ) → ⟨ 𝑋 , 𝑦 ⟩ ∈ ( { 𝑋 } × 𝐴 ) )
17 eleq1 ⊢ ( 𝑍 = ⟨ 𝑋 , 𝑦 ⟩ → ( 𝑍 ∈ ( { 𝑋 } × 𝐴 ) ↔ ⟨ 𝑋 , 𝑦 ⟩ ∈ ( { 𝑋 } × 𝐴 ) ) )
18 16 17 syl5ibrcom ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑍 = ⟨ 𝑋 , 𝑦 ⟩ → 𝑍 ∈ ( { 𝑋 } × 𝐴 ) ) )
19 18 rexlimdva ⊢ ( 𝑋 ∈ 𝑉 → ( ∃ 𝑦 ∈ 𝐴 𝑍 = ⟨ 𝑋 , 𝑦 ⟩ → 𝑍 ∈ ( { 𝑋 } × 𝐴 ) ) )
20 13 19 impbid2 ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑍 ∈ ( { 𝑋 } × 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑍 = ⟨ 𝑋 , 𝑦 ⟩ ) )