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

Theorem mobidv 2316
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 1629 . 2  |-  F/ x ph
2 mobidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2mobid 2315 1  |-  ( ph  ->  ( E* x ps  <->  E* x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E*wmo 2282
This theorem is referenced by:  mobii  2317  mosubopt  4454  dffun6f  5468  funmo  5470  caovmo  6284  1stconst  6435  2ndconst  6436  brdom3  8406  brdom6disj  8410  imasaddfnlem  13753  imasvscafn  13762  hausflim  18013  hausflf  18029  cnextfun  18095  haustsms  18165  limcmo  19769  perfdvf  19790  funressnfv  27968
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554  df-eu 2285  df-mo 2286
  Copyright terms: Public domain W3C validator