Theorem r19.29r 3186

Description: Restricted quantifier version of 19.29r 1878; variation of r19.29 3185. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Wolf Lammen, 29-Jun-2023.)

Assertion

Ref	Expression
r19.29r	⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Proof of Theorem r19.29r

Step	Hyp	Ref	Expression
1		r19.29 3185	. . 3 ⊢ ((∀𝑥 ∈ 𝐴 𝜓 ∧ ∃𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
2	1	ancoms 459	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
3		pm3.22 460	. . 3 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓))
4	3	reximi 3179	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
5	2, 4	syl 17	1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 396  ∀wral 3065  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3070  df-rex 3071

This theorem is referenced by:  r19.29imd  3187  2reu5  3694  rlimuni  15268  rlimno1  15374  neindisj2  22283  lmss  22458  fclsbas  23181  isfcf  23194  ucnima  23442  metcnp3  23705  cfilucfil  23724  bndth  24130  ellimc3  25052  lmxrge0  31911  gsumesum  32036  esumcst  32040  esumfsup  32047  voliune  32206  volfiniune  32207  bnj517  32874  nummin  33072  fvineqsneq  35592  cover2  35881  prmunb2  41936