MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mobidv Structured version   Unicode version

Theorem mobidv 2306
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
StepHypRef Expression
1 nfv 1708 . 2  |-  F/ x ph
2 mobidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2mobid 2304 1  |-  ( ph  ->  ( E* x ps  <->  E* x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E*wmo 2284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-12 1855
This theorem depends on definitions:  df-bi 185  df-ex 1614  df-nf 1618  df-eu 2287  df-mo 2288
This theorem is referenced by:  mobii  2308  mosubopt  4754  dffun6f  5608  funmo  5610  caovmo  6511  1stconst  6887  2ndconst  6888  brdom3  8923  brdom6disj  8927  imasaddfnlem  14944  imasvscafn  14953  hausflim  20607  hausflf  20623  cnextfun  20689  haustsms  20759  limcmo  22411  perfdvf  22432  funressnfv  32374
  Copyright terms: Public domain W3C validator