Proof of Theorem 2uasbanh
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . . . . 5
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) | 
| 2 |  | simprl 771 | . . . . 5
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) → 𝜑) | 
| 3 | 1, 2 | jca 511 | . . . 4
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) | 
| 4 | 3 | 2eximi 1836 | . . 3
⊢
(∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) | 
| 5 |  | simprr 773 | . . . . 5
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) → 𝜓) | 
| 6 | 1, 5 | jca 511 | . . . 4
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)) | 
| 7 | 6 | 2eximi 1836 | . . 3
⊢
(∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)) | 
| 8 | 4, 7 | jca 511 | . 2
⊢
(∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) → (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))) | 
| 9 |  | 2uasbanh.1 | . . 3
⊢ (𝜒 ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))) | 
| 10 | 9 | simplbi 497 | . . . . . 6
⊢ (𝜒 → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) | 
| 11 |  | simpl 482 | . . . . . . . . . 10
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) | 
| 12 | 11 | 2eximi 1836 | . . . . . . . . 9
⊢
(∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) | 
| 13 | 10, 12 | syl 17 | . . . . . . . 8
⊢ (𝜒 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) | 
| 14 |  | ax6e2ndeq 44579 | . . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) | 
| 15 | 13, 14 | sylibr 234 | . . . . . . 7
⊢ (𝜒 → (¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣)) | 
| 16 |  | 2sb5nd 44580 | . . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))) | 
| 17 | 15, 16 | syl 17 | . . . . . 6
⊢ (𝜒 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))) | 
| 18 | 10, 17 | mpbird 257 | . . . . 5
⊢ (𝜒 → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) | 
| 19 | 9 | simprbi 496 | . . . . . 6
⊢ (𝜒 → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)) | 
| 20 |  | 2sb5nd 44580 | . . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))) | 
| 21 | 15, 20 | syl 17 | . . . . . 6
⊢ (𝜒 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))) | 
| 22 | 19, 21 | mpbird 257 | . . . . 5
⊢ (𝜒 → [𝑢 / 𝑥][𝑣 / 𝑦]𝜓) | 
| 23 |  | sban 2080 | . . . . . . 7
⊢ ([𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ ([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓)) | 
| 24 | 23 | sbbii 2076 | . . . . . 6
⊢ ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓)) | 
| 25 |  | sban 2080 | . . . . . 6
⊢ ([𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓)) | 
| 26 | 24, 25 | bitri 275 | . . . . 5
⊢ ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓)) | 
| 27 | 18, 22, 26 | sylanbrc 583 | . . . 4
⊢ (𝜒 → [𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓)) | 
| 28 |  | 2sb5nd 44580 | . . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)))) | 
| 29 | 15, 28 | syl 17 | . . . 4
⊢ (𝜒 → ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)))) | 
| 30 | 27, 29 | mpbid 232 | . . 3
⊢ (𝜒 → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓))) | 
| 31 | 9, 30 | sylbir 235 | . 2
⊢
((∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)) → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓))) | 
| 32 | 8, 31 | impbii 209 | 1
⊢
(∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))) |