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

Theorem moanimv 2338
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 1629 . 2  |-  F/ x ph
21moanim 2336 1  |-  ( E* x ( ph  /\  ps )  <->  ( ph  ->  E* x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   E*wmo 2281
This theorem is referenced by:  2reuswap  3128  2reu5lem2  3132  funmo  5462  funcnv  5503  fncnv  5507  isarep2  5525  fnres  5553  fnopabg  5560  fvopab3ig  5795  opabex  5956  zfrep6  5960  fnoprabg  6163  oprabexd  6178  oprabex  6179  ovidi  6184  ovig  6187  caovmo  6276  th3qcor  7004  nqerf  8797  cnextfun  18085  perfdvf  19780  taylf  20267  2reuswap2  23965  abrexdomjm  23978  mptfnf  24063  abrexdom  26386  2rmoswap  27893
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-6 1744  ax-7 1749  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285
  Copyright terms: Public domain W3C validator