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		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
2		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
3	2	pm5.32ri	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) )
4	3	imbi1i	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) → 𝜑 ) ↔ ( ( 𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) → 𝜑 ) )
5		impexp	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) → 𝜑 ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
6		impexp	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
7	4 5 6	3bitr3i	⊢ ( ( 𝑥 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) ↔ ( 𝐴 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
8	7	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) ↔ ∀ 𝑥 ( 𝐴 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
9		19.21v	⊢ ( ∀ 𝑥 ( 𝐴 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) ↔ ( 𝐴 ∈ 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )
10	1 8 9	3bitri	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )
11	10	a1i	⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) )
12		biimt	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) )
13	12	3ad2ant3	⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) )
14		ceqsalt	⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) )
15	11 13 14	3bitr2d	⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) )