Theorem r19.29r 3096

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3044  ∃wrex 3053

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  r19.29imd  3098  2reu5  3726  rlimuni  15492  rlimno1  15596  neindisj2  22986  lmss  23161  fclsbas  23884  isfcf  23897  ucnima  24144  metcnp3  24404  cfilucfil  24423  bndth  24833  ellimc3  25756  lmxrge0  33915  gsumesum  34022  esumcst  34026  esumfsup  34033  voliune  34192  volfiniune  34193  bnj517  34848  nummin  35054  onvf1odlem1  35063  fvineqsneq  37373  cover2  37682  naddgeoa  43356  prmunb2  44273