Theorem exsb

Description: An equivalent expression for existence. One direction ( exsbim ) needs fewer axioms. (Contributed by NM, 2-Feb-2005) Avoid ax-13 . (Revised by Wolf Lammen, 16-Oct-2022)

	Ref	Expression
Assertion	exsb	|- ( E. x ph <-> E. y A. x ( x = y -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	|- F/ y ph
2		nfa1	|- F/ x A. x ( x = y -> ph )
3		ax12v	|- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
4		sp	|- ( A. x ( x = y -> ph ) -> ( x = y -> ph ) )
5	4	com12	|- ( x = y -> ( A. x ( x = y -> ph ) -> ph ) )
6	3 5	impbid	|- ( x = y -> ( ph <-> A. x ( x = y -> ph ) ) )
7	1 2 6	cbvexv1	|- ( E. x ph <-> E. y A. x ( x = y -> ph ) )