This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )