Theorem r19.29r 3177

Description: Restricted quantifier version of 19.29r 1882; variation of r19.29 3176. (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 3176	. . 3 ⊢ ((∀𝑥 ∈ 𝐴 𝜓 ∧ ∃𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
2	1	ancoms 462	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
3		pm3.22 463	. . 3 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓))
4	3	reximi 3166	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
5	2, 4	syl 17	1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 399  ∀wral 3061  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3066  df-rex 3067

This theorem is referenced by:  r19.29imd  3178  2reu5  3671  rlimuni  15111  rlimno1  15217  neindisj2  22020  lmss  22195  fclsbas  22918  isfcf  22931  ucnima  23178  metcnp3  23438  cfilucfil  23457  bndth  23855  ellimc3  24776  lmxrge0  31616  gsumesum  31739  esumcst  31743  esumfsup  31750  voliune  31909  volfiniune  31910  bnj517  32578  nummin  32776  fvineqsneq  35320  cover2  35609  prmunb2  41602