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

Theorem moanimv 2050
Description: Introduction of a conjunct into at-most-one quantifier. (Contributed by NM, 23-Mar-1995.)
Assertion
Ref Expression
moanimv (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem moanimv
StepHypRef Expression
1 nfv 1491 . 2 𝑥𝜑
21moanim 2049 1 (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  ∃*wmo 1976
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979
This theorem is referenced by:  mosubt  2830  2reuswapdc  2857  2rmorex  2859  mosubopt  4564  funmo  5096  funcnv  5142  fncnv  5147  isarep2  5168  fnres  5197  fnopabg  5204  fvopab3ig  5449  opabex  5598  fnoprabg  5826  ovidi  5843  ovig  5846  oprabexd  5979  oprabex  5980  th3qcor  6487  dvfgg  12612
  Copyright terms: Public domain W3C validator