Theorem mo4 2517

Description: "At most one" expressed using implicit substitution. (Contributed by NM, 26-Jul-1995.)

Hypothesis

Ref	Expression
mo4.1	|- ( x = y -> ( ph <-> ps ) )

Assertion

Ref	Expression
mo4	|- ( E* x ph <-> A. x A. y ( ( ph /\ ps ) -> x = y ) )

Distinct variable groups:   x, y   ph, y   ps, x

Allowed substitution hints:   ph( x)   ps( y)

Proof of Theorem mo4

Step	Hyp	Ref	Expression
1		nfv 1843	. 2 |- F/ x ps
2		mo4.1	. 2 |- ( x = y -> ( ph <-> ps ) )
3	1, 2	mo4f 2516	1 |- ( E* x ph <-> A. x A. y ( ( ph /\ ps ) -> x = y ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   E*wmo 2471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475

This theorem is referenced by:  eu4  2518  rmo4  3399  dffun3  5899  fun11  5963  brprcneu  6184  dff13  6512  mpt2fun  6762  caovmo  6871  wemoiso  7153  wemoiso2  7154  addsrmo  9894  mulsrmo  9895  summo  14448  prodmo  14666  hausflimi  21784  vitalilem3  23379  plyexmo  24068  tglineintmo  25537  ajmoi  27714  pjhthmo  28161  adjmo  28691  moel  29323  noprefixmo  31848  funtransport  32138  funray  32247  funline  32249  lineintmo  32264  dffrege115  38272