Theorem mo4 2036

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 1491	. 2 |- F/ x ps
2		mo4.1	. 2 |- ( x = y -> ( ph <-> ps ) )
3	1, 2	mo4f 2035	1 |- ( E* x ph <-> A. x A. y ( ( ph /\ ps ) -> x = y ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   A.wal 1312   E*wmo 1976

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498

This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979

This theorem is referenced by:  eu4  2037  rmo4  2846  dffun5r  5093  dffun6f  5094  fun11  5148  brprcneu  5368  dff13  5623  mpofun  5827  caovimo  5918  th3qlem1  6485  addnq0mo  7203  mulnq0mo  7204  addsrmo  7486  mulsrmo  7487  summodc  11044  limcimo  12590