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

Theorem mobidv 2294
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 1678 . 2  |-  F/ x ph
2 mobidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2mobid 2292 1  |-  ( ph  ->  ( E* x ps  <->  E* x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E*wmo 2271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-12 1798
This theorem depends on definitions:  df-bi 185  df-ex 1592  df-nf 1595  df-eu 2274  df-mo 2275
This theorem is referenced by:  mobii  2296  mosubopt  4740  dffun6f  5595  funmo  5597  caovmo  6489  1stconst  6863  2ndconst  6864  brdom3  8897  brdom6disj  8901  imasaddfnlem  14774  imasvscafn  14783  hausflim  20212  hausflf  20228  cnextfun  20294  haustsms  20364  limcmo  22016  perfdvf  22037  funressnfv  31637
  Copyright terms: Public domain W3C validator