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

Theorem moanimv 1975
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 1421 . 2  |-  F/ x ph
21moanim 1974 1  |-  ( E* x ( ph  /\  ps )  <->  ( ph  ->  E* x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97    <-> wb 98   E*wmo 1901
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904
This theorem is referenced by:  mosubt  2718  2reuswapdc  2743  2rmorex  2745  mosubopt  4405  funmo  4917  funcnv  4960  fncnv  4965  isarep2  4986  fnres  5015  fnopabg  5022  fvopab3ig  5246  opabex  5385  fnoprabg  5602  ovidi  5619  ovig  5622  oprabexd  5754  oprabex  5755  th3qcor  6210
  Copyright terms: Public domain W3C validator