Theorem reu8nf

Description: Restricted uniqueness using implicit substitution. This version of reu8 uses a nonfreeness hypothesis for x and ps instead of distinct variable conditions. (Contributed by AV, 21-Jan-2022)

	Ref	Expression
Hypotheses	reu8nf.1	|- F/ x ps
	reu8nf.2	|- F/ x ch
	reu8nf.3	|- ( x = w -> ( ph <-> ch ) )
	reu8nf.4	|- ( w = y -> ( ch <-> ps ) )
Assertion	reu8nf	|- ( E! x e. A ph <-> E. x e. A ( ph /\ A. y e. A ( ps -> x = y ) ) )

Proof

Step	Hyp	Ref	Expression
1		reu8nf.1	|- F/ x ps
2		reu8nf.2	|- F/ x ch
3		reu8nf.3	|- ( x = w -> ( ph <-> ch ) )
4		reu8nf.4	|- ( w = y -> ( ch <-> ps ) )
5		nfv	|- F/ w ph
6	5 2 3	cbvreuw	|- ( E! x e. A ph <-> E! w e. A ch )
7	4	reu8	|- ( E! w e. A ch <-> E. w e. A ( ch /\ A. y e. A ( ps -> w = y ) ) )
8		nfcv	|- F/_ x A
9		nfv	|- F/ x w = y
10	1 9	nfim	|- F/ x ( ps -> w = y )
11	8 10	nfralw	|- F/ x A. y e. A ( ps -> w = y )
12	2 11	nfan	|- F/ x ( ch /\ A. y e. A ( ps -> w = y ) )
13		nfv	|- F/ w ( ph /\ A. y e. A ( ps -> x = y ) )
14	3	bicomd	|- ( x = w -> ( ch <-> ph ) )
15	14	equcoms	|- ( w = x -> ( ch <-> ph ) )
16		equequ1	|- ( w = x -> ( w = y <-> x = y ) )
17	16	imbi2d	|- ( w = x -> ( ( ps -> w = y ) <-> ( ps -> x = y ) ) )
18	17	ralbidv	|- ( w = x -> ( A. y e. A ( ps -> w = y ) <-> A. y e. A ( ps -> x = y ) ) )
19	15 18	anbi12d	|- ( w = x -> ( ( ch /\ A. y e. A ( ps -> w = y ) ) <-> ( ph /\ A. y e. A ( ps -> x = y ) ) ) )
20	12 13 19	cbvrexw	|- ( E. w e. A ( ch /\ A. y e. A ( ps -> w = y ) ) <-> E. x e. A ( ph /\ A. y e. A ( ps -> x = y ) ) )
21	6 7 20	3bitri	|- ( E! x e. A ph <-> E. x e. A ( ph /\ A. y e. A ( ps -> x = y ) ) )