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

Theorem moanimv 1957
Description: Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 23-Mar-1995.)
Assertion
Ref Expression
moanimv (∃*x(φ ψ) ↔ (φ∃*xψ))
Distinct variable group:   φ,x
Allowed substitution hint:   ψ(x)

Proof of Theorem moanimv
StepHypRef Expression
1 nfv 1402 . 2 xφ
21moanim 1956 1 (∃*x(φ ψ) ↔ (φ∃*xψ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98  ∃*wmo 1883
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 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886
This theorem is referenced by:  mosubt  2695  2reuswapdc  2720  2rmorex  2722  mosubopt  4332  funmo  4843  funcnv  4886  fncnv  4891  isarep2  4912  fnres  4941  fnopabg  4948  fvopab3ig  5171  opabex  5310  fnoprabg  5525  ovidi  5542  ovig  5545  oprabexd  5677  oprabex  5678  th3qcor  6121
  Copyright terms: Public domain W3C validator