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

Theorem moanimv 2330
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 1754 . 2  |-  F/ x ph
21moanim 2328 1  |-  ( E* x ( ph  /\  ps )  <->  ( ph  ->  E* x ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370   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-10 1889  ax-12 1907
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-ex 1660  df-nf 1664  df-eu 2270  df-mo 2271
This theorem is referenced by:  2reuswap  3280  2reu5lem2  3284  funmo  5617  funcnv  5661  fncnv  5665  isarep2  5681  fnres  5710  mptfnf  5717  fnopabg  5719  fvopab3ig  5961  opabex  6149  fnoprabg  6411  ovidi  6429  ovig  6432  caovmo  6520  zfrep6  6775  oprabexd  6794  oprabex  6795  nqerf  9354  cnextfun  21010  perfdvf  22735  taylf  23181  2reuswap2  27959  abrexdomjm  27977  abrexdom  31761  2rmoswap  37996
  Copyright terms: Public domain W3C validator