Theorem axextmo

Description: There exists at most one set with prescribed elements. Theorem 1.1 of BellMachover p. 462. (Contributed by NM, 30-Jun-1994) (Proof shortened by Wolf Lammen, 13-Nov-2019) Use the at-most-one quantifier. (Revised by BJ, 17-Sep-2022)

	Ref	Expression
Hypothesis	axextmo.1	|- F/ x ph
Assertion	axextmo	|- E* x A. y ( y e. x <-> ph )

Proof

Step	Hyp	Ref	Expression
1		axextmo.1	|- F/ x ph
2		biantr	|- ( ( ( y e. x <-> ph ) /\ ( y e. z <-> ph ) ) -> ( y e. x <-> y e. z ) )
3	2	alanimi	|- ( ( A. y ( y e. x <-> ph ) /\ A. y ( y e. z <-> ph ) ) -> A. y ( y e. x <-> y e. z ) )
4		ax-ext	|- ( A. y ( y e. x <-> y e. z ) -> x = z )
5	3 4	syl	|- ( ( A. y ( y e. x <-> ph ) /\ A. y ( y e. z <-> ph ) ) -> x = z )
6	5	gen2	|- A. x A. z ( ( A. y ( y e. x <-> ph ) /\ A. y ( y e. z <-> ph ) ) -> x = z )
7		nfv	|- F/ x y e. z
8	7 1	nfbi	|- F/ x ( y e. z <-> ph )
9	8	nfal	|- F/ x A. y ( y e. z <-> ph )
10		elequ2	|- ( x = z -> ( y e. x <-> y e. z ) )
11	10	bibi1d	|- ( x = z -> ( ( y e. x <-> ph ) <-> ( y e. z <-> ph ) ) )
12	11	albidv	|- ( x = z -> ( A. y ( y e. x <-> ph ) <-> A. y ( y e. z <-> ph ) ) )
13	9 12	mo4f	|- ( E* x A. y ( y e. x <-> ph ) <-> A. x A. z ( ( A. y ( y e. x <-> ph ) /\ A. y ( y e. z <-> ph ) ) -> x = z ) )
14	6 13	mpbir	|- E* x A. y ( y e. x <-> ph )