Theorem mo4 2337

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

Hypothesis

Ref	Expression
mo4.1

Assertion

Ref	Expression
mo4

Distinct variable groups:   ,   ,   ,

Proof of Theorem mo4

Step	Hyp	Ref	Expression
1		nfv 1707	. 2
2		mo4.1	. 2
3	1, 2	mo4f 2336	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E*wmo 2283

This theorem is referenced by:  eu4  2338  rmo4  3292  dffun3  5604  fun11  5658  brprcneu  5864  dff13  6166  mpt2fun  6404  caovmo  6512  wemoiso  6785  wemoiso2  6786  addsrmo  9471  mulsrmo  9472  summo  13539  prodmo  13743  hausflimi  20481  vitalilem3  22019  plyexmo  22709  tglineintmo  24022  frg2wot1  25057  ajmoi  25774  pjhthmo  26220  adjmo  26751  moel  27382  funtransport  29681  funray  29790  funline  29792  lineintmo  29807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287