Step |
Hyp |
Ref |
Expression |
1 |
|
eqer.1 |
⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 ) |
2 |
|
eqer.2 |
⊢ 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ 𝐴 = 𝐵 } |
3 |
2
|
relopabiv |
⊢ Rel 𝑅 |
4 |
|
id |
⊢ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 ) |
5 |
4
|
eqcomd |
⊢ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 → ⦋ 𝑤 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) |
6 |
1 2
|
eqerlem |
⊢ ( 𝑧 𝑅 𝑤 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 ) |
7 |
1 2
|
eqerlem |
⊢ ( 𝑤 𝑅 𝑧 ↔ ⦋ 𝑤 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) |
8 |
5 6 7
|
3imtr4i |
⊢ ( 𝑧 𝑅 𝑤 → 𝑤 𝑅 𝑧 ) |
9 |
|
eqtr |
⊢ ( ( ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 ∧ ⦋ 𝑤 / 𝑥 ⦌ 𝐴 = ⦋ 𝑣 / 𝑥 ⦌ 𝐴 ) → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑣 / 𝑥 ⦌ 𝐴 ) |
10 |
1 2
|
eqerlem |
⊢ ( 𝑤 𝑅 𝑣 ↔ ⦋ 𝑤 / 𝑥 ⦌ 𝐴 = ⦋ 𝑣 / 𝑥 ⦌ 𝐴 ) |
11 |
6 10
|
anbi12i |
⊢ ( ( 𝑧 𝑅 𝑤 ∧ 𝑤 𝑅 𝑣 ) ↔ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 ∧ ⦋ 𝑤 / 𝑥 ⦌ 𝐴 = ⦋ 𝑣 / 𝑥 ⦌ 𝐴 ) ) |
12 |
1 2
|
eqerlem |
⊢ ( 𝑧 𝑅 𝑣 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑣 / 𝑥 ⦌ 𝐴 ) |
13 |
9 11 12
|
3imtr4i |
⊢ ( ( 𝑧 𝑅 𝑤 ∧ 𝑤 𝑅 𝑣 ) → 𝑧 𝑅 𝑣 ) |
14 |
|
vex |
⊢ 𝑧 ∈ V |
15 |
|
eqid |
⊢ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 |
16 |
1 2
|
eqerlem |
⊢ ( 𝑧 𝑅 𝑧 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) |
17 |
15 16
|
mpbir |
⊢ 𝑧 𝑅 𝑧 |
18 |
14 17
|
2th |
⊢ ( 𝑧 ∈ V ↔ 𝑧 𝑅 𝑧 ) |
19 |
3 8 13 18
|
iseri |
⊢ 𝑅 Er V |