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 ⊢ X ∈ V → Z ∈ X × A ↔ ∃ y ∈ A Z = X y

Proof

Step Hyp Ref Expression
1 elxp ⊢ Z ∈ X × A ↔ ∃ x ∃ y Z = x y ∧ x ∈ X ∧ y ∈ A
2 df-rex ⊢ ∃ y ∈ A x ∈ X ∧ Z = x y ↔ ∃ y y ∈ A ∧ x ∈ X ∧ Z = x y
3 an13 ⊢ Z = x y ∧ x ∈ X ∧ y ∈ A ↔ y ∈ A ∧ x ∈ X ∧ Z = x y
4 3 exbii ⊢ ∃ y Z = x y ∧ x ∈ X ∧ y ∈ A ↔ ∃ y y ∈ A ∧ x ∈ X ∧ Z = x y
5 2 4 bitr4i ⊢ ∃ y ∈ A x ∈ X ∧ Z = x y ↔ ∃ y Z = x y ∧ x ∈ X ∧ y ∈ A
6 elsni ⊢ x ∈ X → x = X
7 6 opeq1d ⊢ x ∈ X → x y = X y
8 7 eqeq2d ⊢ x ∈ X → Z = x y ↔ Z = X y
9 8 biimpa ⊢ x ∈ X ∧ Z = x y → Z = X y
10 9 reximi ⊢ ∃ y ∈ A x ∈ X ∧ Z = x y → ∃ y ∈ A Z = X y
11 5 10 sylbir ⊢ ∃ y Z = x y ∧ x ∈ X ∧ y ∈ A → ∃ y ∈ A Z = X y
12 11 exlimiv ⊢ ∃ x ∃ y Z = x y ∧ x ∈ X ∧ y ∈ A → ∃ y ∈ A Z = X y
13 1 12 sylbi ⊢ Z ∈ X × A → ∃ y ∈ A Z = X y
14 snidg ⊢ X ∈ V → X ∈ X
15 opelxpi ⊢ X ∈ X ∧ y ∈ A → X y ∈ X × A
16 14 15 sylan ⊢ X ∈ V ∧ y ∈ A → X y ∈ X × A
17 eleq1 ⊢ Z = X y → Z ∈ X × A ↔ X y ∈ X × A
18 16 17 syl5ibrcom ⊢ X ∈ V ∧ y ∈ A → Z = X y → Z ∈ X × A
19 18 rexlimdva ⊢ X ∈ V → ∃ y ∈ A Z = X y → Z ∈ X × A
20 13 19 impbid2 ⊢ X ∈ V → Z ∈ X × A ↔ ∃ y ∈ A Z = X y