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	|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> ( A. x e. B ( x = A -> ph ) <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		biimt	|- ( A e. B -> ( A. x ( x = A -> ph ) <-> ( A e. B -> A. x ( x = A -> ph ) ) ) )
2		df-ral	|- ( A. x e. B ( x = A -> ph ) <-> A. x ( x e. B -> ( x = A -> ph ) ) )
3		eleq1	|- ( x = A -> ( x e. B <-> A e. B ) )
4	3	pm5.32ri	|- ( ( x e. B /\ x = A ) <-> ( A e. B /\ x = A ) )
5	4	imbi1i	|- ( ( ( x e. B /\ x = A ) -> ph ) <-> ( ( A e. B /\ x = A ) -> ph ) )
6		impexp	|- ( ( ( x e. B /\ x = A ) -> ph ) <-> ( x e. B -> ( x = A -> ph ) ) )
7		impexp	|- ( ( ( A e. B /\ x = A ) -> ph ) <-> ( A e. B -> ( x = A -> ph ) ) )
8	5 6 7	3bitr3i	|- ( ( x e. B -> ( x = A -> ph ) ) <-> ( A e. B -> ( x = A -> ph ) ) )
9	8	albii	|- ( A. x ( x e. B -> ( x = A -> ph ) ) <-> A. x ( A e. B -> ( x = A -> ph ) ) )
10		19.21v	|- ( A. x ( A e. B -> ( x = A -> ph ) ) <-> ( A e. B -> A. x ( x = A -> ph ) ) )
11	2 9 10	3bitrri	|- ( ( A e. B -> A. x ( x = A -> ph ) ) <-> A. x e. B ( x = A -> ph ) )
12	1 11	bitrdi	|- ( A e. B -> ( A. x ( x = A -> ph ) <-> A. x e. B ( x = A -> ph ) ) )
13	12	3ad2ant3	|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> ( A. x ( x = A -> ph ) <-> A. x e. B ( x = A -> ph ) ) )
14		ceqsalt	|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> ( A. x ( x = A -> ph ) <-> ps ) )
15	13 14	bitr3d	|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> ( A. x e. B ( x = A -> ph ) <-> ps ) )