Theorem wl-cbvalnaed

Description: wl-cbvalnae with a context. (Contributed by Wolf Lammen, 28-Jul-2019)

	Ref	Expression
Hypotheses	wl-cbvalnaed.1	|- F/ x ph
	wl-cbvalnaed.2	|- F/ y ph
	wl-cbvalnaed.3	|- ( ph -> ( -. A. x x = y -> F/ y ps ) )
	wl-cbvalnaed.4	|- ( ph -> ( -. A. x x = y -> F/ x ch ) )
	wl-cbvalnaed.5	|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
Assertion	wl-cbvalnaed	|- ( ph -> ( A. x ps <-> A. y ch ) )

Proof

Step	Hyp	Ref	Expression
1		wl-cbvalnaed.1	|- F/ x ph
2		wl-cbvalnaed.2	|- F/ y ph
3		wl-cbvalnaed.3	|- ( ph -> ( -. A. x x = y -> F/ y ps ) )
4		wl-cbvalnaed.4	|- ( ph -> ( -. A. x x = y -> F/ x ch ) )
5		wl-cbvalnaed.5	|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
6	1 2 5	wl-dral1d	|- ( ph -> ( A. x x = y -> ( A. x ps <-> A. y ch ) ) )
7	6	imp	|- ( ( ph /\ A. x x = y ) -> ( A. x ps <-> A. y ch ) )
8		nfnae	|- F/ x -. A. x x = y
9	1 8	nfan	|- F/ x ( ph /\ -. A. x x = y )
10		wl-nfnae1	|- F/ y -. A. x x = y
11	2 10	nfan	|- F/ y ( ph /\ -. A. x x = y )
12	3	imp	|- ( ( ph /\ -. A. x x = y ) -> F/ y ps )
13	4	imp	|- ( ( ph /\ -. A. x x = y ) -> F/ x ch )
14	5	adantr	|- ( ( ph /\ -. A. x x = y ) -> ( x = y -> ( ps <-> ch ) ) )
15	9 11 12 13 14	cbv2	|- ( ( ph /\ -. A. x x = y ) -> ( A. x ps <-> A. y ch ) )
16	7 15	pm2.61dan	|- ( ph -> ( A. x ps <-> A. y ch ) )