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

Theorem moanimv 2611
Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2612 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 528 . . 3 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21mobidv 2539 . 2 (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑𝜓)))
3 simpl 482 . . 3 ((𝜑𝜓) → 𝜑)
43exlimiv 1926 . 2 (∃𝑥(𝜑𝜓) → 𝜑)
52, 4moanimlem 2610 1 (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  ∃*wmo 2528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-mo 2530
This theorem is referenced by:  2reuswap  3741  2reuswap2  3742  2reu5lem2  3751  2rmoswap  3756  funmo  6568  funmoOLD  6569  funcnv  6622  fncnv  6626  isarep2  6644  fnres  6682  mptfnf  6690  fnopabg  6692  fvopab3ig  7001  opabex  7232  fnoprabg  7543  ovidi  7564  ovig  7567  caovmo  7658  zfrep6  7958  oprabexd  7979  oprabex  7980  nqerf  10953  cnextfun  23967  perfdvf  25831  taylf  26294  reuxfrdf  32288  abrexdomjm  32301  abrexdom  37203
  Copyright terms: Public domain W3C validator