Metamath Proof Explorer

Theorem 2mos

Description: Double "there exists at most one", using implicit substitution. (Contributed by NM, 10-Feb-2005) (Proof shortened by Wolf Lammen, 21-May-2025)

Ref Expression
Hypothesis 2mos.1 ⊢ x = z ∧ y = w → φ ↔ ψ
Assertion 2mos ⊢ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w ↔ ∀ x ∀ y ∀ z ∀ w φ ∧ ψ → x = z ∧ y = w

Proof

Step Hyp Ref Expression
1 2mos.1 ⊢ x = z ∧ y = w → φ ↔ ψ
2 2mo ⊢ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w ↔ ∀ x ∀ y ∀ z ∀ w φ ∧ z x w y φ → x = z ∧ y = w
3 1 2sbievw ⊢ z x w y φ ↔ ψ
4 3 anbi2i ⊢ φ ∧ z x w y φ ↔ φ ∧ ψ
5 4 imbi1i ⊢ φ ∧ z x w y φ → x = z ∧ y = w ↔ φ ∧ ψ → x = z ∧ y = w
6 5 2albii ⊢ ∀ z ∀ w φ ∧ z x w y φ → x = z ∧ y = w ↔ ∀ z ∀ w φ ∧ ψ → x = z ∧ y = w
7 6 2albii ⊢ ∀ x ∀ y ∀ z ∀ w φ ∧ z x w y φ → x = z ∧ y = w ↔ ∀ x ∀ y ∀ z ∀ w φ ∧ ψ → x = z ∧ y = w
8 2 7 bitri ⊢ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w ↔ ∀ x ∀ y ∀ z ∀ w φ ∧ ψ → x = z ∧ y = w