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

Theorem moanimv 1991
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 1437 . 2 𝑥𝜑
21moanim 1990 1 (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102  ∃*wmo 1917
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920
This theorem is referenced by:  mosubt  2741  2reuswapdc  2766  2rmorex  2768  mosubopt  4433  funmo  4945  funcnv  4988  fncnv  4993  isarep2  5014  fnres  5043  fnopabg  5050  fvopab3ig  5274  opabex  5413  fnoprabg  5630  ovidi  5647  ovig  5650  oprabexd  5782  oprabex  5783  th3qcor  6241
  Copyright terms: Public domain W3C validator