Theorem ceqsralv2

Description: Alternate elimination of a restricted universal quantifier, using implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020)

	Ref	Expression
Hypothesis	ceqsralv2.1	|- ( x = A -> ( ph <-> ps ) )
Assertion	ceqsralv2	|- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		ceqsralv2.1	|- ( x = A -> ( ph <-> ps ) )
2	1	notbid	|- ( x = A -> ( -. ph <-> -. ps ) )
3	2	ceqsrexv2	|- ( E. x e. B ( x = A /\ -. ph ) <-> ( A e. B /\ -. ps ) )
4		rexanali	|- ( E. x e. B ( x = A /\ -. ph ) <-> -. A. x e. B ( x = A -> ph ) )
5		annim	|- ( ( A e. B /\ -. ps ) <-> -. ( A e. B -> ps ) )
6	3 4 5	3bitr3i	|- ( -. A. x e. B ( x = A -> ph ) <-> -. ( A e. B -> ps ) )
7	6	con4bii	|- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) )