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

Theorem moanimv 2371
Description: Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 23-Mar-1995.)
Assertion
Ref Expression
moanimv  |-  ( E* x ( ph  /\  ps )  <->  ( ph  ->  E* x ps ) )
Distinct variable group:    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem moanimv
StepHypRef Expression
1 nfv 1772 . 2  |-  F/ x ph
21moanim 2369 1  |-  ( E* x ( ph  /\  ps )  <->  ( ph  ->  E* x ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375   E*wmo 2311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-ex 1675  df-nf 1679  df-eu 2314  df-mo 2315
This theorem is referenced by:  2reuswap  3254  2reu5lem2  3258  funmo  5617  funcnv  5665  fncnv  5669  isarep2  5685  fnres  5714  mptfnf  5721  fnopabg  5723  fvopab3ig  5968  opabex  6159  fnoprabg  6424  ovidi  6442  ovig  6445  caovmo  6533  zfrep6  6788  oprabexd  6807  oprabex  6808  nqerf  9381  cnextfun  21128  perfdvf  22907  taylf  23365  2reuswap2  28173  abrexdomjm  28190  abrexdom  32102  2rmoswap  38643
  Copyright terms: Public domain W3C validator