| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | erth.1 | . . . . . . . 8
⊢ (𝜑 → 𝑅 Er 𝑋) | 
| 2 | 1 | ersymb 8759 | . . . . . . 7
⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴)) | 
| 3 | 2 | biimpa 476 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → 𝐵𝑅𝐴) | 
| 4 | 1 | ertr 8760 | . . . . . . 7
⊢ (𝜑 → ((𝐵𝑅𝐴 ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥)) | 
| 5 | 4 | impl 455 | . . . . . 6
⊢ (((𝜑 ∧ 𝐵𝑅𝐴) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥) | 
| 6 | 3, 5 | syldanl 602 | . . . . 5
⊢ (((𝜑 ∧ 𝐴𝑅𝐵) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥) | 
| 7 | 1 | ertr 8760 | . . . . . 6
⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝑥) → 𝐴𝑅𝑥)) | 
| 8 | 7 | impl 455 | . . . . 5
⊢ (((𝜑 ∧ 𝐴𝑅𝐵) ∧ 𝐵𝑅𝑥) → 𝐴𝑅𝑥) | 
| 9 | 6, 8 | impbida 801 | . . . 4
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → (𝐴𝑅𝑥 ↔ 𝐵𝑅𝑥)) | 
| 10 |  | vex 3484 | . . . . 5
⊢ 𝑥 ∈ V | 
| 11 |  | erth.2 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑋) | 
| 12 | 11 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ 𝑋) | 
| 13 |  | elecg 8789 | . . . . 5
⊢ ((𝑥 ∈ V ∧ 𝐴 ∈ 𝑋) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝑥)) | 
| 14 | 10, 12, 13 | sylancr 587 | . . . 4
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝑥)) | 
| 15 |  | errel 8754 | . . . . . . 7
⊢ (𝑅 Er 𝑋 → Rel 𝑅) | 
| 16 | 1, 15 | syl 17 | . . . . . 6
⊢ (𝜑 → Rel 𝑅) | 
| 17 |  | brrelex2 5739 | . . . . . 6
⊢ ((Rel
𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V) | 
| 18 | 16, 17 | sylan 580 | . . . . 5
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V) | 
| 19 |  | elecg 8789 | . . . . 5
⊢ ((𝑥 ∈ V ∧ 𝐵 ∈ V) → (𝑥 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝑥)) | 
| 20 | 10, 18, 19 | sylancr 587 | . . . 4
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → (𝑥 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝑥)) | 
| 21 | 9, 14, 20 | 3bitr4d 311 | . . 3
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝑥 ∈ [𝐵]𝑅)) | 
| 22 | 21 | eqrdv 2735 | . 2
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → [𝐴]𝑅 = [𝐵]𝑅) | 
| 23 | 1 | adantr 480 | . . 3
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝑅 Er 𝑋) | 
| 24 | 1, 11 | erref 8765 | . . . . . . 7
⊢ (𝜑 → 𝐴𝑅𝐴) | 
| 25 | 24 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐴) | 
| 26 | 11 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ 𝑋) | 
| 27 |  | elecg 8789 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝐴)) | 
| 28 | 26, 26, 27 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝐴)) | 
| 29 | 25, 28 | mpbird 257 | . . . . 5
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐴]𝑅) | 
| 30 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅) | 
| 31 | 29, 30 | eleqtrd 2843 | . . . 4
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐵]𝑅) | 
| 32 | 23, 30 | ereldm 8795 | . . . . . 6
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋)) | 
| 33 | 26, 32 | mpbid 232 | . . . . 5
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵 ∈ 𝑋) | 
| 34 |  | elecg 8789 | . . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) | 
| 35 | 26, 33, 34 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) | 
| 36 | 31, 35 | mpbid 232 | . . 3
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵𝑅𝐴) | 
| 37 | 23, 36 | ersym 8757 | . 2
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐵) | 
| 38 | 22, 37 | impbida 801 | 1
⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅)) |