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

Theorem mobidv 2191
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 1609 . 2  |-  F/ x ph
2 mobidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2mobid 2190 1  |-  ( ph  ->  ( E* x ps  <->  E* x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E*wmo 2157
This theorem is referenced by:  mobii  2192  mosubopt  4280  dffun6f  5285  funmo  5287  caovmo  6073  1stconst  6223  2ndconst  6224  brdom3  8169  brdom6disj  8173  imasaddfnlem  13446  imasvscafn  13455  hausflim  17692  hausflf  17708  haustsms  17834  limcmo  19248  perfdvf  19269  funressnfv  28096
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-ex 1532  df-nf 1535  df-eu 2160  df-mo 2161
  Copyright terms: Public domain W3C validator