Theorem wl-cbvalnae

Description: A more general version of cbval when nonfree properties depend on a distinctor. Such expressions arise in proofs aiming at the elimination of distinct variable constraints, specifically in application of dvelimf , nfsb2 or dveeq1 . (Contributed by Wolf Lammen, 4-Jun-2019)

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

Proof

Step	Hyp	Ref	Expression
1		wl-cbvalnae.1	|- ( -. A. x x = y -> F/ y ph )
2		wl-cbvalnae.2	|- ( -. A. x x = y -> F/ x ps )
3		wl-cbvalnae.3	|- ( x = y -> ( ph <-> ps ) )
4		nftru	|- F/ x T.
5		nftru	|- F/ y T.
6	1	a1i	|- ( T. -> ( -. A. x x = y -> F/ y ph ) )
7	2	a1i	|- ( T. -> ( -. A. x x = y -> F/ x ps ) )
8	3	a1i	|- ( T. -> ( x = y -> ( ph <-> ps ) ) )
9	4 5 6 7 8	wl-cbvalnaed	|- ( T. -> ( A. x ph <-> A. y ps ) )
10	9	mptru	|- ( A. x ph <-> A. y ps )