Theorem ceqsralt

Description: Restricted quantifier version of ceqsalt . (Contributed by NM, 28-Feb-2013) (Revised by Mario Carneiro, 10-Oct-2016)

	Ref	Expression
Assertion	ceqsralt	⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		biimt	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) )
2		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
3		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
4	3	pm5.32ri	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) )
5	4	imbi1i	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) → 𝜑 ) ↔ ( ( 𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) → 𝜑 ) )
6		impexp	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) → 𝜑 ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
7		impexp	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
8	5 6 7	3bitr3i	⊢ ( ( 𝑥 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) ↔ ( 𝐴 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
9	8	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) ↔ ∀ 𝑥 ( 𝐴 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
10		19.21v	⊢ ( ∀ 𝑥 ( 𝐴 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) ↔ ( 𝐴 ∈ 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )
11	2 9 10	3bitrri	⊢ ( ( 𝐴 ∈ 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 → 𝜑 ) )
12	1 11	bitrdi	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 → 𝜑 ) ) )
13	12	3ad2ant3	⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 → 𝜑 ) ) )
14		ceqsalt	⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) )
15	13 14	bitr3d	⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) )