Theorem r19.29r 3103

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3051  ∃wrex 3060

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 3052  df-rex 3061

This theorem is referenced by:  r19.29imd  3105  2reu5  3741  rlimuni  15564  rlimno1  15668  neindisj2  23059  lmss  23234  fclsbas  23957  isfcf  23970  ucnima  24217  metcnp3  24477  cfilucfil  24496  bndth  24906  ellimc3  25830  lmxrge0  33929  gsumesum  34036  esumcst  34040  esumfsup  34047  voliune  34206  volfiniune  34207  bnj517  34862  nummin  35068  fvineqsneq  37376  cover2  37685  naddgeoa  43365  prmunb2  44283