Step |
Hyp |
Ref |
Expression |
1 |
|
xpsff1o.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ { 〈 ∅ , 𝑥 〉 , 〈 1o , 𝑦 〉 } ) |
2 |
|
simpl |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑥 = 𝑋 ) |
3 |
2
|
opeq2d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 〈 ∅ , 𝑥 〉 = 〈 ∅ , 𝑋 〉 ) |
4 |
|
simpr |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 ) |
5 |
4
|
opeq2d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 〈 1o , 𝑦 〉 = 〈 1o , 𝑌 〉 ) |
6 |
3 5
|
preq12d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → { 〈 ∅ , 𝑥 〉 , 〈 1o , 𝑦 〉 } = { 〈 ∅ , 𝑋 〉 , 〈 1o , 𝑌 〉 } ) |
7 |
|
prex |
⊢ { 〈 ∅ , 𝑋 〉 , 〈 1o , 𝑌 〉 } ∈ V |
8 |
6 1 7
|
ovmpoa |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐹 𝑌 ) = { 〈 ∅ , 𝑋 〉 , 〈 1o , 𝑌 〉 } ) |