Proof of Theorem 2pm13.193VD
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | idn1 44594 | . . . . 5
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ) | 
| 2 |  | simpl 482 | . . . . 5
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) | 
| 3 | 1, 2 | e1a 44647 | . . . 4
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ) | 
| 4 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢) | 
| 5 | 3, 4 | e1a 44647 | . . . . . . . . . 10
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   𝑥 = 𝑢   ) | 
| 6 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) | 
| 7 | 1, 6 | e1a 44647 | . . . . . . . . . 10
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜑   ) | 
| 8 |  | pm3.21 471 | . . . . . . . . . 10
⊢ (𝑥 = 𝑢 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ 𝑥 = 𝑢))) | 
| 9 | 5, 7, 8 | e11 44708 | . . . . . . . . 9
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ 𝑥 = 𝑢)   ) | 
| 10 |  | sbequ2 2249 | . . . . . . . . . 10
⊢ (𝑥 = 𝑢 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑣 / 𝑦]𝜑)) | 
| 11 | 10 | imdistanri 569 | . . . . . . . . 9
⊢ (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ 𝑥 = 𝑢) → ([𝑣 / 𝑦]𝜑 ∧ 𝑥 = 𝑢)) | 
| 12 | 9, 11 | e1a 44647 | . . . . . . . 8
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ([𝑣 / 𝑦]𝜑 ∧ 𝑥 = 𝑢)   ) | 
| 13 |  | simpl 482 | . . . . . . . 8
⊢ (([𝑣 / 𝑦]𝜑 ∧ 𝑥 = 𝑢) → [𝑣 / 𝑦]𝜑) | 
| 14 | 12, 13 | e1a 44647 | . . . . . . 7
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   [𝑣 / 𝑦]𝜑   ) | 
| 15 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣) | 
| 16 | 3, 15 | e1a 44647 | . . . . . . 7
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   𝑦 = 𝑣   ) | 
| 17 |  | pm3.2 469 | . . . . . . 7
⊢ ([𝑣 / 𝑦]𝜑 → (𝑦 = 𝑣 → ([𝑣 / 𝑦]𝜑 ∧ 𝑦 = 𝑣))) | 
| 18 | 14, 16, 17 | e11 44708 | . . . . . 6
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ([𝑣 / 𝑦]𝜑 ∧ 𝑦 = 𝑣)   ) | 
| 19 |  | sbequ2 2249 | . . . . . . 7
⊢ (𝑦 = 𝑣 → ([𝑣 / 𝑦]𝜑 → 𝜑)) | 
| 20 | 19 | imdistanri 569 | . . . . . 6
⊢ (([𝑣 / 𝑦]𝜑 ∧ 𝑦 = 𝑣) → (𝜑 ∧ 𝑦 = 𝑣)) | 
| 21 | 18, 20 | e1a 44647 | . . . . 5
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   (𝜑 ∧ 𝑦 = 𝑣)   ) | 
| 22 |  | simpl 482 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 = 𝑣) → 𝜑) | 
| 23 | 21, 22 | e1a 44647 | . . . 4
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   𝜑   ) | 
| 24 |  | pm3.2 469 | . . . 4
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝜑 → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))) | 
| 25 | 3, 23, 24 | e11 44708 | . . 3
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ) | 
| 26 | 25 | in1 44591 | . 2
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) | 
| 27 |  | idn1 44594 | . . . . 5
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ) | 
| 28 |  | simpl 482 | . . . . 5
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) | 
| 29 | 27, 28 | e1a 44647 | . . . 4
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ) | 
| 30 | 29, 4 | e1a 44647 | . . . . . . 7
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ▶   𝑥 = 𝑢   ) | 
| 31 | 29, 15 | e1a 44647 | . . . . . . . . . 10
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ▶   𝑦 = 𝑣   ) | 
| 32 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) → 𝜑) | 
| 33 | 27, 32 | e1a 44647 | . . . . . . . . . 10
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ▶   𝜑   ) | 
| 34 |  | pm3.21 471 | . . . . . . . . . 10
⊢ (𝑦 = 𝑣 → (𝜑 → (𝜑 ∧ 𝑦 = 𝑣))) | 
| 35 | 31, 33, 34 | e11 44708 | . . . . . . . . 9
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ▶   (𝜑 ∧ 𝑦 = 𝑣)   ) | 
| 36 |  | sbequ1 2248 | . . . . . . . . . 10
⊢ (𝑦 = 𝑣 → (𝜑 → [𝑣 / 𝑦]𝜑)) | 
| 37 | 36 | imdistanri 569 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = 𝑣) → ([𝑣 / 𝑦]𝜑 ∧ 𝑦 = 𝑣)) | 
| 38 | 35, 37 | e1a 44647 | . . . . . . . 8
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ▶   ([𝑣 / 𝑦]𝜑 ∧ 𝑦 = 𝑣)   ) | 
| 39 |  | simpl 482 | . . . . . . . 8
⊢ (([𝑣 / 𝑦]𝜑 ∧ 𝑦 = 𝑣) → [𝑣 / 𝑦]𝜑) | 
| 40 | 38, 39 | e1a 44647 | . . . . . . 7
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ▶   [𝑣 / 𝑦]𝜑   ) | 
| 41 |  | pm3.21 471 | . . . . . . 7
⊢ (𝑥 = 𝑢 → ([𝑣 / 𝑦]𝜑 → ([𝑣 / 𝑦]𝜑 ∧ 𝑥 = 𝑢))) | 
| 42 | 30, 40, 41 | e11 44708 | . . . . . 6
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ▶   ([𝑣 / 𝑦]𝜑 ∧ 𝑥 = 𝑢)   ) | 
| 43 |  | sbequ1 2248 | . . . . . . 7
⊢ (𝑥 = 𝑢 → ([𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) | 
| 44 | 43 | imdistanri 569 | . . . . . 6
⊢ (([𝑣 / 𝑦]𝜑 ∧ 𝑥 = 𝑢) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ 𝑥 = 𝑢)) | 
| 45 | 42, 44 | e1a 44647 | . . . . 5
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ 𝑥 = 𝑢)   ) | 
| 46 |  | simpl 482 | . . . . 5
⊢ (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ 𝑥 = 𝑢) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) | 
| 47 | 45, 46 | e1a 44647 | . . . 4
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜑   ) | 
| 48 |  | pm3.2 469 | . . . 4
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))) | 
| 49 | 29, 47, 48 | e11 44708 | . . 3
⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ) | 
| 50 | 49 | in1 44591 | . 2
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) | 
| 51 | 26, 50 | impbii 209 | 1
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) |