Step |
Hyp |
Ref |
Expression |
1 |
|
gaorb.1 |
⊢ ∼ = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } |
2 |
|
oveq2 |
⊢ ( 𝑥 = 𝐴 → ( 𝑔 ⊕ 𝑥 ) = ( 𝑔 ⊕ 𝐴 ) ) |
3 |
|
eqeq12 |
⊢ ( ( ( 𝑔 ⊕ 𝑥 ) = ( 𝑔 ⊕ 𝐴 ) ∧ 𝑦 = 𝐵 ) → ( ( 𝑔 ⊕ 𝑥 ) = 𝑦 ↔ ( 𝑔 ⊕ 𝐴 ) = 𝐵 ) ) |
4 |
2 3
|
sylan |
⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑔 ⊕ 𝑥 ) = 𝑦 ↔ ( 𝑔 ⊕ 𝐴 ) = 𝐵 ) ) |
5 |
4
|
rexbidv |
⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ↔ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝐴 ) = 𝐵 ) ) |
6 |
|
oveq1 |
⊢ ( 𝑔 = ℎ → ( 𝑔 ⊕ 𝐴 ) = ( ℎ ⊕ 𝐴 ) ) |
7 |
6
|
eqeq1d |
⊢ ( 𝑔 = ℎ → ( ( 𝑔 ⊕ 𝐴 ) = 𝐵 ↔ ( ℎ ⊕ 𝐴 ) = 𝐵 ) ) |
8 |
7
|
cbvrexvw |
⊢ ( ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝐴 ) = 𝐵 ↔ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐵 ) |
9 |
5 8
|
bitrdi |
⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ↔ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐵 ) ) |
10 |
|
vex |
⊢ 𝑥 ∈ V |
11 |
|
vex |
⊢ 𝑦 ∈ V |
12 |
10 11
|
prss |
⊢ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝑌 ) |
13 |
12
|
anbi1i |
⊢ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) ) |
14 |
13
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } |
15 |
1 14
|
eqtr4i |
⊢ ∼ = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } |
16 |
9 15
|
brab2a |
⊢ ( 𝐴 ∼ 𝐵 ↔ ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐵 ) ) |
17 |
|
df-3an |
⊢ ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐵 ) ↔ ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐵 ) ) |
18 |
16 17
|
bitr4i |
⊢ ( 𝐴 ∼ 𝐵 ↔ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐵 ) ) |