Theorem moanimv 2530

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

Step	Hyp	Ref	Expression
1		nfv 1840	. 2 ⊢ Ⅎ𝑥𝜑
2	1	moanim 2528	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  ∃*wmo 2470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-12 2044

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-eu 2473  df-mo 2474

This theorem is referenced by:  2reuswap  3397  2reu5lem2  3401  funmo  5873  funcnv  5926  fncnv  5930  isarep2  5946  fnres  5975  mptfnf  5982  fnopabg  5984  fvopab3ig  6245  opabex  6448  fnoprabg  6726  ovidi  6744  ovig  6747  caovmo  6836  zfrep6  7096  oprabexd  7115  oprabex  7116  nqerf  9712  cnextfun  21808  perfdvf  23607  taylf  24053  2reuswap2  29217  abrexdomjm  29233  abrexdom  33196  2rmoswap  40518