This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm13.192

Description: Theorem *13.192 in WhiteheadRussell p. 179. (Contributed by Andrew Salmon, 3-Jun-2011) (Revised by NM, 4-Jan-2017)

Ref Expression
Assertion pm13.192 ⊢ ∃ y ∀ x x = A ↔ x = y ∧ φ ↔ [˙A / y]˙ φ

Proof

Step Hyp Ref Expression
1 biimpr ⊢ x = A ↔ x = y → x = y → x = A
2 1 alimi ⊢ ∀ x x = A ↔ x = y → ∀ x x = y → x = A
3 eqeq1 ⊢ x = y → x = A ↔ y = A
4 3 equsalvw ⊢ ∀ x x = y → x = A ↔ y = A
5 2 4 sylib ⊢ ∀ x x = A ↔ x = y → y = A
6 eqeq2 ⊢ A = y → x = A ↔ x = y
7 6 eqcoms ⊢ y = A → x = A ↔ x = y
8 7 alrimiv ⊢ y = A → ∀ x x = A ↔ x = y
9 5 8 impbii ⊢ ∀ x x = A ↔ x = y ↔ y = A
10 9 anbi1i ⊢ ∀ x x = A ↔ x = y ∧ φ ↔ y = A ∧ φ
11 10 exbii ⊢ ∃ y ∀ x x = A ↔ x = y ∧ φ ↔ ∃ y y = A ∧ φ
12 sbc5 ⊢ [˙A / y]˙ φ ↔ ∃ y y = A ∧ φ
13 11 12 bitr4i ⊢ ∃ y ∀ x x = A ↔ x = y ∧ φ ↔ [˙A / y]˙ φ