Theorem rspceb2dv

Description: Restricted existential specialization, using implicit substitution in both directions. (Contributed by Zhi Wang, 28-Sep-2024)

	Ref	Expression
Hypotheses	rspceb2dv.1	|- ( ( ph /\ x e. B ) -> ( ps -> ch ) )
	rspceb2dv.2	|- ( ( ph /\ ch ) -> A e. B )
	rspceb2dv.3	|- ( ( ph /\ ch ) -> th )
	rspceb2dv.4	|- ( x = A -> ( ps <-> th ) )
Assertion	rspceb2dv	|- ( ph -> ( E. x e. B ps <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		rspceb2dv.1	|- ( ( ph /\ x e. B ) -> ( ps -> ch ) )
2		rspceb2dv.2	|- ( ( ph /\ ch ) -> A e. B )
3		rspceb2dv.3	|- ( ( ph /\ ch ) -> th )
4		rspceb2dv.4	|- ( x = A -> ( ps <-> th ) )
5	1	rexlimdva	|- ( ph -> ( E. x e. B ps -> ch ) )
6	4	rspcev	|- ( ( A e. B /\ th ) -> E. x e. B ps )
7	2 3 6	syl2anc	|- ( ( ph /\ ch ) -> E. x e. B ps )
8	7	ex	|- ( ph -> ( ch -> E. x e. B ps ) )
9	5 8	impbid	|- ( ph -> ( E. x e. B ps <-> ch ) )