Theorem r19.29r 3096

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3047  ∃wrex 3056

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 3048  df-rex 3057

This theorem is referenced by:  r19.29imd  3097  2reu5  3712  rlimuni  15452  rlimno1  15556  neindisj2  23033  lmss  23208  fclsbas  23931  isfcf  23944  ucnima  24190  metcnp3  24450  cfilucfil  24469  bndth  24879  ellimc3  25802  lmxrge0  33957  gsumesum  34064  esumcst  34068  esumfsup  34075  voliune  34234  volfiniune  34235  bnj517  34889  nummin  35096  onvf1odlem1  35139  fvineqsneq  37446  cover2  37755  naddgeoa  43427  prmunb2  44344