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