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