Theorem r19.29r 3097

Description: Restricted quantifier version of 19.29r 1875; variation of r19.29 3096. (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		iba 527	. . 3 ⊢ (𝜓 → (𝜑 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3090	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpac 478	1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3048  ∃wrex 3057

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3049  df-rex 3058

This theorem is referenced by:  r19.29imd  3098  2reu5  3713  rlimuni  15464  rlimno1  15568  neindisj2  23058  lmss  23233  fclsbas  23956  isfcf  23969  ucnima  24215  metcnp3  24475  cfilucfil  24494  bndth  24904  ellimc3  25827  lmxrge0  34037  gsumesum  34144  esumcst  34148  esumfsup  34155  voliune  34314  volfiniune  34315  bnj517  34969  nummin  35176  onvf1odlem1  35219  fvineqsneq  37529  cover2  37828  naddgeoa  43551  prmunb2  44468