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

Theorem mobidv 2289
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 1754 . 2  |-  F/ x ph
2 mobidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2mobid 2287 1  |-  ( ph  ->  ( E* x ps  <->  E* x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   E*wmo 2267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-12 1907
This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664  df-eu 2270  df-mo 2271
This theorem is referenced by:  mobii  2291  mosubopt  4719  dffun6f  5615  funmo  5617  caovmo  6520  1stconst  6895  2ndconst  6896  brdom3  8954  brdom6disj  8958  imasaddfnlem  15385  imasvscafn  15394  hausflim  20927  hausflf  20943  cnextfun  21010  haustsms  21081  limcmo  22714  perfdvf  22735  phpreu  31633  funressnfv  38020
  Copyright terms: Public domain W3C validator