Theorem ralbinrald

Description: Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017)

	Ref	Expression
Hypotheses	ralbinrald.1	|- ( ph -> X e. A )
	ralbinrald.2	|- ( x e. A -> x = X )
	ralbinrald.3	|- ( x = X -> ( ps <-> th ) )
Assertion	ralbinrald	|- ( ph -> ( A. x e. A ps <-> th ) )

Proof

Step	Hyp	Ref	Expression
1		ralbinrald.1	|- ( ph -> X e. A )
2		ralbinrald.2	|- ( x e. A -> x = X )
3		ralbinrald.3	|- ( x = X -> ( ps <-> th ) )
4	3	adantl	|- ( ( ph /\ x = X ) -> ( ps <-> th ) )
5	1 4	rspcdv	|- ( ph -> ( A. x e. A ps -> th ) )
6	3	bicomd	|- ( x = X -> ( th <-> ps ) )
7	2 6	syl	|- ( x e. A -> ( th <-> ps ) )
8	7	adantl	|- ( ( ph /\ x e. A ) -> ( th <-> ps ) )
9	8	biimpd	|- ( ( ph /\ x e. A ) -> ( th -> ps ) )
10	9	ralrimdva	|- ( ph -> ( th -> A. x e. A ps ) )
11	5 10	impbid	|- ( ph -> ( A. x e. A ps <-> th ) )