Theorem mo4 2080

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023

This theorem is referenced by:  eu4  2081  rmo4  2923  dffun5r  5208  dffun6f  5209  fun11  5263  brprcneu  5487  dff13  5744  mpofun  5952  caovimo  6043  th3qlem1  6611  addnq0mo  7396  mulnq0mo  7397  addsrmo  7692  mulsrmo  7693  summodc  11333  prodmodc  11528  limcimo  13387