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 ( 𝑋𝑉 → ( 𝑍 ∈ ( { 𝑋 } × 𝐴 ) ↔ ∃ 𝑦𝐴 𝑍 = ⟨ 𝑋 , 𝑦 ⟩ ) )