Metamath Proof Explorer

Theorem 2mos

Description: Double "there exists at most one", using implicit substitution. (Contributed by NM, 10-Feb-2005)

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 nfv ⊢ Ⅎ y x = z
4 3 sbrim ⊢ w y x = z → φ ↔ x = z → w y φ
5 1 expcom ⊢ y = w → x = z → φ ↔ ψ
6 5 pm5.74d ⊢ y = w → x = z → φ ↔ x = z → ψ
7 6 sbievw ⊢ w y x = z → φ ↔ x = z → ψ
8 4 7 bitr3i ⊢ x = z → w y φ ↔ x = z → ψ
9 8 pm5.74ri ⊢ x = z → w y φ ↔ ψ
10 9 sbievw ⊢ z x w y φ ↔ ψ
11 10 anbi2i ⊢ φ ∧ z x w y φ ↔ φ ∧ ψ
12 11 imbi1i ⊢ φ ∧ z x w y φ → x = z ∧ y = w ↔ φ ∧ ψ → x = z ∧ y = w
13 12 2albii ⊢ ∀ z ∀ w φ ∧ z x w y φ → x = z ∧ y = w ↔ ∀ z ∀ w φ ∧ ψ → x = z ∧ y = w
14 13 2albii ⊢ ∀ x ∀ y ∀ z ∀ w φ ∧ z x w y φ → x = z ∧ y = w ↔ ∀ x ∀ y ∀ z ∀ w φ ∧ ψ → x = z ∧ y = w
15 2 14 bitri ⊢ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w ↔ ∀ x ∀ y ∀ z ∀ w φ ∧ ψ → x = z ∧ y = w