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

Theorem mobidv 2284
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 1674 . 2  |-  F/ x ph
2 mobidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2mobid 2282 1  |-  ( ph  ->  ( E* x ps  <->  E* x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E*wmo 2261
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591  df-eu 2264  df-mo 2265
This theorem is referenced by:  mobii  2286  mosubopt  4689  dffun6f  5532  funmo  5534  caovmo  6402  1stconst  6763  2ndconst  6764  brdom3  8798  brdom6disj  8802  imasaddfnlem  14570  imasvscafn  14579  hausflim  19672  hausflf  19688  cnextfun  19754  haustsms  19824  limcmo  21475  perfdvf  21496  funressnfv  30174
  Copyright terms: Public domain W3C validator