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

Metamath Proof Explorer

Theorem pm14.122b

Description: Theorem *14.122 in WhiteheadRussell p. 185. (Contributed by Andrew Salmon, 9-Jun-2011)

Ref Expression
Assertion pm14.122b ⊢ A ∈ V → ∀ x φ → x = A ∧ [˙A / x]˙ φ ↔ ∀ x φ → x = A ∧ ∃ x φ

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ y = A → x = y ↔ x = A
2 1 imbi2d ⊢ y = A → φ → x = y ↔ φ → x = A
3 2 albidv ⊢ y = A → ∀ x φ → x = y ↔ ∀ x φ → x = A
4 dfsbcq ⊢ y = A → [˙y / x]˙ φ ↔ [˙A / x]˙ φ
5 4 bibi1d ⊢ y = A → [˙y / x]˙ φ ↔ ∃ x φ ↔ [˙A / x]˙ φ ↔ ∃ x φ
6 3 5 imbi12d ⊢ y = A → ∀ x φ → x = y → [˙y / x]˙ φ ↔ ∃ x φ ↔ ∀ x φ → x = A → [˙A / x]˙ φ ↔ ∃ x φ
7 sbc5 ⊢ [˙y / x]˙ φ ↔ ∃ x x = y ∧ φ
8 nfa1 ⊢ Ⅎ x ∀ x φ → x = y
9 simpr ⊢ x = y ∧ φ → φ
10 ancr ⊢ φ → x = y → φ → x = y ∧ φ
11 10 sps ⊢ ∀ x φ → x = y → φ → x = y ∧ φ
12 9 11 impbid2 ⊢ ∀ x φ → x = y → x = y ∧ φ ↔ φ
13 8 12 exbid ⊢ ∀ x φ → x = y → ∃ x x = y ∧ φ ↔ ∃ x φ
14 7 13 bitrid ⊢ ∀ x φ → x = y → [˙y / x]˙ φ ↔ ∃ x φ
15 6 14 vtoclg ⊢ A ∈ V → ∀ x φ → x = A → [˙A / x]˙ φ ↔ ∃ x φ
16 15 pm5.32d ⊢ A ∈ V → ∀ x φ → x = A ∧ [˙A / x]˙ φ ↔ ∀ x φ → x = A ∧ ∃ x φ