Step |
Hyp |
Ref |
Expression |
1 |
|
dfima3 |
⊢ ( ◡ 𝑅 “ ( V ∖ { 𝑍 } ) ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ∧ 〈 𝑦 , 𝑥 〉 ∈ ◡ 𝑅 ) } |
2 |
|
eldifvsn |
⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ↔ 𝑦 ≠ 𝑍 ) ) |
3 |
2
|
elv |
⊢ ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ↔ 𝑦 ≠ 𝑍 ) |
4 |
|
vex |
⊢ 𝑦 ∈ V |
5 |
|
vex |
⊢ 𝑥 ∈ V |
6 |
4 5
|
opelcnv |
⊢ ( 〈 𝑦 , 𝑥 〉 ∈ ◡ 𝑅 ↔ 〈 𝑥 , 𝑦 〉 ∈ 𝑅 ) |
7 |
|
df-br |
⊢ ( 𝑥 𝑅 𝑦 ↔ 〈 𝑥 , 𝑦 〉 ∈ 𝑅 ) |
8 |
6 7
|
bitr4i |
⊢ ( 〈 𝑦 , 𝑥 〉 ∈ ◡ 𝑅 ↔ 𝑥 𝑅 𝑦 ) |
9 |
3 8
|
anbi12ci |
⊢ ( ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ∧ 〈 𝑦 , 𝑥 〉 ∈ ◡ 𝑅 ) ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) ) |
10 |
9
|
exbii |
⊢ ( ∃ 𝑦 ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ∧ 〈 𝑦 , 𝑥 〉 ∈ ◡ 𝑅 ) ↔ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) ) |
11 |
10
|
abbii |
⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ∧ 〈 𝑦 , 𝑥 〉 ∈ ◡ 𝑅 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) } |
12 |
1 11
|
eqtri |
⊢ ( ◡ 𝑅 “ ( V ∖ { 𝑍 } ) ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) } |