Step |
Hyp |
Ref |
Expression |
1 |
|
vex |
⊢ 𝑧 ∈ V |
2 |
|
vex |
⊢ 𝑤 ∈ V |
3 |
|
opeq1 |
⊢ ( 𝑥 = 𝑧 → 〈 𝑥 , 𝑦 〉 = 〈 𝑧 , 𝑦 〉 ) |
4 |
3
|
eleq1d |
⊢ ( 𝑥 = 𝑧 → ( 〈 𝑥 , 𝑦 〉 ∈ 𝐴 ↔ 〈 𝑧 , 𝑦 〉 ∈ 𝐴 ) ) |
5 |
|
opeq2 |
⊢ ( 𝑦 = 𝑤 → 〈 𝑧 , 𝑦 〉 = 〈 𝑧 , 𝑤 〉 ) |
6 |
5
|
eleq1d |
⊢ ( 𝑦 = 𝑤 → ( 〈 𝑧 , 𝑦 〉 ∈ 𝐴 ↔ 〈 𝑧 , 𝑤 〉 ∈ 𝐴 ) ) |
7 |
1 2 4 6
|
opelopab |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 〈 𝑥 , 𝑦 〉 ∈ 𝐴 } ↔ 〈 𝑧 , 𝑤 〉 ∈ 𝐴 ) |
8 |
7
|
gen2 |
⊢ ∀ 𝑧 ∀ 𝑤 ( 〈 𝑧 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 〈 𝑥 , 𝑦 〉 ∈ 𝐴 } ↔ 〈 𝑧 , 𝑤 〉 ∈ 𝐴 ) |
9 |
|
relopab |
⊢ Rel { 〈 𝑥 , 𝑦 〉 ∣ 〈 𝑥 , 𝑦 〉 ∈ 𝐴 } |
10 |
|
eqrel |
⊢ ( ( Rel { 〈 𝑥 , 𝑦 〉 ∣ 〈 𝑥 , 𝑦 〉 ∈ 𝐴 } ∧ Rel 𝐴 ) → ( { 〈 𝑥 , 𝑦 〉 ∣ 〈 𝑥 , 𝑦 〉 ∈ 𝐴 } = 𝐴 ↔ ∀ 𝑧 ∀ 𝑤 ( 〈 𝑧 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 〈 𝑥 , 𝑦 〉 ∈ 𝐴 } ↔ 〈 𝑧 , 𝑤 〉 ∈ 𝐴 ) ) ) |
11 |
9 10
|
mpan |
⊢ ( Rel 𝐴 → ( { 〈 𝑥 , 𝑦 〉 ∣ 〈 𝑥 , 𝑦 〉 ∈ 𝐴 } = 𝐴 ↔ ∀ 𝑧 ∀ 𝑤 ( 〈 𝑧 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 〈 𝑥 , 𝑦 〉 ∈ 𝐴 } ↔ 〈 𝑧 , 𝑤 〉 ∈ 𝐴 ) ) ) |
12 |
8 11
|
mpbiri |
⊢ ( Rel 𝐴 → { 〈 𝑥 , 𝑦 〉 ∣ 〈 𝑥 , 𝑦 〉 ∈ 𝐴 } = 𝐴 ) |