Step |
Hyp |
Ref |
Expression |
1 |
|
relcnv |
⊢ Rel ◡ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } |
2 |
|
relopabv |
⊢ Rel { 〈 𝑦 , 𝑥 〉 ∣ 𝜑 } |
3 |
|
vopelopabsb |
⊢ ( 〈 𝑤 , 𝑧 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ) |
4 |
|
sbcom2 |
⊢ ( [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] [ 𝑤 / 𝑥 ] 𝜑 ) |
5 |
3 4
|
bitri |
⊢ ( 〈 𝑤 , 𝑧 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ [ 𝑧 / 𝑦 ] [ 𝑤 / 𝑥 ] 𝜑 ) |
6 |
|
vex |
⊢ 𝑧 ∈ V |
7 |
|
vex |
⊢ 𝑤 ∈ V |
8 |
6 7
|
opelcnv |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ ◡ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ 〈 𝑤 , 𝑧 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ) |
9 |
|
vopelopabsb |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ { 〈 𝑦 , 𝑥 〉 ∣ 𝜑 } ↔ [ 𝑧 / 𝑦 ] [ 𝑤 / 𝑥 ] 𝜑 ) |
10 |
5 8 9
|
3bitr4i |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ ◡ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ 〈 𝑧 , 𝑤 〉 ∈ { 〈 𝑦 , 𝑥 〉 ∣ 𝜑 } ) |
11 |
1 2 10
|
eqrelriiv |
⊢ ◡ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } = { 〈 𝑦 , 𝑥 〉 ∣ 𝜑 } |