MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  moanimv Structured version   Visualization version   GIF version

Theorem moanimv 2701
Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2702 requiring disjoint variables, but fewer axioms. (Contributed by NM, 23-Mar-1995.) Reduce axiom usage . (Revised by Wolf Lammen, 8-Feb-2023.)
Assertion
Ref Expression
moanimv (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem moanimv
StepHypRef Expression
1 ibar 529 . . 3 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21mobidv 2627 . 2 (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑𝜓)))
3 simpl 483 . . 3 ((𝜑𝜓) → 𝜑)
43exlimiv 1924 . 2 (∃𝑥(𝜑𝜓) → 𝜑)
52, 4moanimlem 2700 1 (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  ∃*wmo 2613
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-mo 2615
This theorem is referenced by:  2reuswap  3740  2reuswap2  3741  2reu5lem2  3750  2rmoswap  3755  funmo  6367  funcnv  6419  fncnv  6423  isarep2  6439  fnres  6470  mptfnf  6479  fnopabg  6481  fvopab3ig  6760  opabex  6981  fnoprabg  7268  ovidi  7286  ovig  7289  caovmo  7378  zfrep6  7650  oprabexd  7670  oprabex  7671  nqerf  10344  cnextfun  22588  perfdvf  24416  taylf  24864  reuxfrdf  30170  abrexdomjm  30182  abrexdom  34874
  Copyright terms: Public domain W3C validator