Theorem mobidv 2305

Description: Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by Mario Carneiro, 7-Oct-2016.)

Hypothesis

Ref	Expression
mobidv.1

Assertion

Ref	Expression
mobidv

Distinct variable group:   ,

Proof of Theorem mobidv

Step	Hyp	Ref	Expression
1		nfv 1707	. 2
2		mobidv.1	. 2
3	1, 2	mobid 2303	1

Syntax hints:  ->wi 4  <->wb 184  E*wmo 2283

This theorem is referenced by:  mobii  2307  mosubopt  4750  dffun6f  5607  funmo  5609  caovmo  6512  1stconst  6888  2ndconst  6889  brdom3  8927  brdom6disj  8931  imasaddfnlem  14925  imasvscafn  14934  hausflim  20482  hausflf  20498  cnextfun  20564  haustsms  20634  limcmo  22286  perfdvf  22307  funressnfv  32213

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-12 1854

This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617  df-eu 2286  df-mo 2287