Step |
Hyp |
Ref |
Expression |
1 |
|
dfrefrels3 |
⊢ RefRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∈ dom 𝑟 ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 = 𝑦 → 𝑥 𝑟 𝑦 ) } |
2 |
|
dmeq |
⊢ ( 𝑟 = 𝑅 → dom 𝑟 = dom 𝑅 ) |
3 |
|
rneq |
⊢ ( 𝑟 = 𝑅 → ran 𝑟 = ran 𝑅 ) |
4 |
|
breq |
⊢ ( 𝑟 = 𝑅 → ( 𝑥 𝑟 𝑦 ↔ 𝑥 𝑅 𝑦 ) ) |
5 |
4
|
imbi2d |
⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 = 𝑦 → 𝑥 𝑟 𝑦 ) ↔ ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ) ) |
6 |
3 5
|
raleqbidv |
⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 = 𝑦 → 𝑥 𝑟 𝑦 ) ↔ ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ) ) |
7 |
2 6
|
raleqbidv |
⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑥 ∈ dom 𝑟 ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 = 𝑦 → 𝑥 𝑟 𝑦 ) ↔ ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ) ) |
8 |
1 7
|
rabeqel |
⊢ ( 𝑅 ∈ RefRels ↔ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ∧ 𝑅 ∈ Rels ) ) |