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 ( 𝐴 ∈ 𝑉 → ( ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) ∧ ∃ 𝑥 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 ) )
2 1 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( 𝜑 → 𝑥 = 𝑦 ) ↔ ( 𝜑 → 𝑥 = 𝐴 ) ) )
3 2 albidv ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) ) )
4 dfsbcq ⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
5 4 bibi1d ⊢ ( 𝑦 = 𝐴 → ( ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 𝜑 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 𝜑 ) ) )
6 3 5 imbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 𝜑 ) ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 𝜑 ) ) ) )
7 sbc5 ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
8 nfa1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 )
9 simpr ⊢ ( ( 𝑥 = 𝑦 ∧ 𝜑 ) → 𝜑 )
10 ancr ⊢ ( ( 𝜑 → 𝑥 = 𝑦 ) → ( 𝜑 → ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
11 10 sps ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( 𝜑 → ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
12 9 11 impbid2 ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ 𝜑 ) )
13 8 12 exbid ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ∃ 𝑥 𝜑 ) )
14 7 13 bitrid ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 𝜑 ) )
15 6 14 vtoclg ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 𝜑 ) ) )
16 15 pm5.32d ⊢ ( 𝐴 ∈ 𝑉 → ( ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) ∧ ∃ 𝑥 𝜑 ) ) )