Theorem r19.29r 3184

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3063  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  r19.29imd  3185  2reu5  3688  rlimuni  15187  rlimno1  15293  neindisj2  22182  lmss  22357  fclsbas  23080  isfcf  23093  ucnima  23341  metcnp3  23602  cfilucfil  23621  bndth  24027  ellimc3  24948  lmxrge0  31804  gsumesum  31927  esumcst  31931  esumfsup  31938  voliune  32097  volfiniune  32098  bnj517  32765  nummin  32963  fvineqsneq  35510  cover2  35799  prmunb2  41818