Theorem cbveuw

Description: Version of cbveu with a disjoint variable condition, which does not require ax-10 , ax-13 . (Contributed by NM, 25-Nov-1994) (Revised by GG, 23-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbveuw.1	|- F/ y ph
2		cbveuw.2	|- F/ x ps
3		cbveuw.3	|- ( x = y -> ( ph <-> ps ) )
4	1 2 3	cbvexv1	|- ( E. x ph <-> E. y ps )
5	1 2 3	cbvmow	|- ( 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 )