Theorem cbveuALT

Description: Alternative proof of cbveu . Since df-eu combines two other quantifiers, one can base this theorem on their associated 'change bounded variable' kind of theorems as well. (Contributed by Wolf Lammen, 5-Jan-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbveu.1	|- F/ y ph
	cbveu.2	|- F/ x ps
	cbveu.3	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbveuALT	|- ( E! x ph <-> E! y ps )

Proof

Step	Hyp	Ref	Expression
1		cbveu.1	|- F/ y ph
2		cbveu.2	|- F/ x ps
3		cbveu.3	|- ( x = y -> ( ph <-> ps ) )
4	1 2 3	cbvex	|- ( E. x ph <-> E. y ps )
5	1 2 3	cbvmo	|- ( E* x ph <-> E* y ps )
6	4 5	anbi12i	|- ( ( E. x ph /\ E* x ph ) <-> ( E. y ps /\ E* y ps ) )
7		df-eu	|- ( E! x ph <-> ( E. x ph /\ E* x ph ) )
8		df-eu	|- ( E! y ps <-> ( E. y ps /\ E* y ps ) )
9	6 7 8	3bitr4i	|- ( E! x ph <-> E! y ps )