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	syl5bb	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 𝜑 ) )
15	6 14	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 𝜑 ) ) )
16	15	pm5.32d	⊢ ( 𝐴 ∈ 𝑉 → ( ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝐴 ) ∧ ∃ 𝑥 𝜑 ) ) )