Theorem mobidv 2491

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

Hypothesis

Ref	Expression
mobidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
mobidv	|- ( ph -> ( E* x ps <-> E* x ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem mobidv

Step	Hyp	Ref	Expression
1		nfv 1843	. 2 |- F/ x ph
2		mobidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	mobid 2489	1 |- ( ph -> ( E* x ps <-> E* x ch ) )

Syntax hints:   -> wi 4   <-> wb 196   E*wmo 2471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710  df-eu 2474  df-mo 2475

This theorem is referenced by:  mobii  2493  mosubopt  4972  dffun6f  5902  funmo  5904  caovmo  6871  1stconst  7265  2ndconst  7266  brdom3  9350  brdom6disj  9354  imasaddfnlem  16188  imasvscafn  16197  hausflim  21785  hausflf  21801  cnextfun  21868  haustsms  21939  limcmo  23646  perfdvf  23667  phpreu  33393  alrmomo2  34124  funressnfv  41208