ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  moanimv Unicode version

Theorem moanimv 2052
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 1493 . 2  |-  F/ x ph
21moanim 2051 1  |-  ( E* x ( ph  /\  ps )  <->  ( ph  ->  E* x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104   E*wmo 1978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981
This theorem is referenced by:  mosubt  2834  2reuswapdc  2861  2rmorex  2863  mosubopt  4574  funmo  5108  funcnv  5154  fncnv  5159  isarep2  5180  fnres  5209  fnopabg  5216  fvopab3ig  5463  opabex  5612  fnoprabg  5840  ovidi  5857  ovig  5860  oprabexd  5993  oprabex  5994  th3qcor  6501  dvfgg  12753
  Copyright terms: Public domain W3C validator