Step |
Hyp |
Ref |
Expression |
1 |
|
relcnv |
⊢ Rel ◡ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } |
2 |
|
relopabv |
⊢ Rel { 〈 𝑦 , 𝑥 〉 ∣ 𝜑 } |
3 |
|
elopab |
⊢ ( 〈 𝑤 , 𝑧 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( 〈 𝑤 , 𝑧 〉 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) |
4 |
|
excom |
⊢ ( ∃ 𝑥 ∃ 𝑦 ( 〈 𝑤 , 𝑧 〉 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑥 ( 〈 𝑤 , 𝑧 〉 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) |
5 |
|
ancom |
⊢ ( ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ↔ ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) ) |
6 |
|
vex |
⊢ 𝑤 ∈ V |
7 |
|
vex |
⊢ 𝑧 ∈ V |
8 |
6 7
|
opth |
⊢ ( 〈 𝑤 , 𝑧 〉 = 〈 𝑥 , 𝑦 〉 ↔ ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ) |
9 |
7 6
|
opth |
⊢ ( 〈 𝑧 , 𝑤 〉 = 〈 𝑦 , 𝑥 〉 ↔ ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) ) |
10 |
5 8 9
|
3bitr4i |
⊢ ( 〈 𝑤 , 𝑧 〉 = 〈 𝑥 , 𝑦 〉 ↔ 〈 𝑧 , 𝑤 〉 = 〈 𝑦 , 𝑥 〉 ) |
11 |
10
|
anbi1i |
⊢ ( ( 〈 𝑤 , 𝑧 〉 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ↔ ( 〈 𝑧 , 𝑤 〉 = 〈 𝑦 , 𝑥 〉 ∧ 𝜑 ) ) |
12 |
11
|
2exbii |
⊢ ( ∃ 𝑦 ∃ 𝑥 ( 〈 𝑤 , 𝑧 〉 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑥 ( 〈 𝑧 , 𝑤 〉 = 〈 𝑦 , 𝑥 〉 ∧ 𝜑 ) ) |
13 |
3 4 12
|
3bitri |
⊢ ( 〈 𝑤 , 𝑧 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ ∃ 𝑦 ∃ 𝑥 ( 〈 𝑧 , 𝑤 〉 = 〈 𝑦 , 𝑥 〉 ∧ 𝜑 ) ) |
14 |
7 6
|
opelcnv |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ ◡ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ 〈 𝑤 , 𝑧 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ) |
15 |
|
elopab |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ { 〈 𝑦 , 𝑥 〉 ∣ 𝜑 } ↔ ∃ 𝑦 ∃ 𝑥 ( 〈 𝑧 , 𝑤 〉 = 〈 𝑦 , 𝑥 〉 ∧ 𝜑 ) ) |
16 |
13 14 15
|
3bitr4i |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ ◡ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ 〈 𝑧 , 𝑤 〉 ∈ { 〈 𝑦 , 𝑥 〉 ∣ 𝜑 } ) |
17 |
1 2 16
|
eqrelriiv |
⊢ ◡ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } = { 〈 𝑦 , 𝑥 〉 ∣ 𝜑 } |