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

Theorem moanimv 2214
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 1609 . 2  |-  F/ x ph
21moanim 2212 1  |-  ( E* x ( ph  /\  ps )  <->  ( ph  ->  E* x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   E*wmo 2157
This theorem is referenced by:  2reuswap  2980  2reu5lem2  2984  funmo  5287  funcnv  5326  fncnv  5330  isarep2  5348  fnres  5376  fnopabg  5383  fvopab3ig  5615  opabex  5760  zfrep6  5764  fnoprabg  5961  oprabexd  5976  oprabex  5977  ovidi  5982  ovig  5985  caovmo  6073  th3qcor  6782  nqerf  8570  perfdvf  19269  taylf  19756  2reuswap2  23153  abrexdomjm  23181  mptfnf  23241  abrexdom  26508  2rmoswap  28065
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-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161
  Copyright terms: Public domain W3C validator