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  5210  dffun6f  5211  fun11  5265  brprcneu  5489  dff13  5747  mpofun  5955  caovimo  6046  th3qlem1  6615  addnq0mo  7409  mulnq0mo  7410  addsrmo  7705  mulsrmo  7706  summodc  11346  prodmodc  11541  limcimo  13428