Step |
Hyp |
Ref |
Expression |
1 |
|
elpredim.1 |
⊢ 𝑋 ∈ V |
2 |
|
df-pred |
⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) |
3 |
2
|
elin2 |
⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) ) |
4 |
|
elimasng |
⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) → ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ↔ 〈 𝑋 , 𝑌 〉 ∈ ◡ 𝑅 ) ) |
5 |
|
opelcnvg |
⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) → ( 〈 𝑋 , 𝑌 〉 ∈ ◡ 𝑅 ↔ 〈 𝑌 , 𝑋 〉 ∈ 𝑅 ) ) |
6 |
4 5
|
bitrd |
⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) → ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ↔ 〈 𝑌 , 𝑋 〉 ∈ 𝑅 ) ) |
7 |
1 6
|
mpan |
⊢ ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) → ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ↔ 〈 𝑌 , 𝑋 〉 ∈ 𝑅 ) ) |
8 |
7
|
ibi |
⊢ ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) → 〈 𝑌 , 𝑋 〉 ∈ 𝑅 ) |
9 |
|
df-br |
⊢ ( 𝑌 𝑅 𝑋 ↔ 〈 𝑌 , 𝑋 〉 ∈ 𝑅 ) |
10 |
8 9
|
sylibr |
⊢ ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) → 𝑌 𝑅 𝑋 ) |
11 |
3 10
|
simplbiim |
⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑌 𝑅 𝑋 ) |