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

Theorem moanimv 2640
 Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2641 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 532 . . 3 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21mobidv 2567 . 2 (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑𝜓)))
3 simpl 486 . . 3 ((𝜑𝜓) → 𝜑)
43exlimiv 1931 . 2 (∃𝑥(𝜑𝜓) → 𝜑)
52, 4moanimlem 2639 1 (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∃*wmo 2555 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-mo 2557 This theorem is referenced by:  2reuswap  3660  2reuswap2  3661  2reu5lem2  3670  2rmoswap  3675  funmo  6351  funcnv  6404  fncnv  6408  isarep2  6424  fnres  6457  mptfnf  6466  fnopabg  6468  fvopab3ig  6755  opabex  6974  fnoprabg  7269  ovidi  7288  ovig  7291  caovmo  7381  zfrep6  7660  oprabexd  7680  oprabex  7681  nqerf  10390  cnextfun  22764  perfdvf  24602  taylf  25055  reuxfrdf  30361  abrexdomjm  30374  abrexdom  35448
 Copyright terms: Public domain W3C validator