Theorem r19.29r 3131

Description: Restricted quantifier version of 19.29r 1907; variation of r19.29 3130. (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 537	. . 3 ⊢ (𝜓 → (𝜑 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3124	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpac 484	1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wral 3081  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3082  df-rex 3092

This theorem is used by:  r19.29imd  3132  2reu5  3723  rlimuni  15627  rlimno1  15731  neindisj2  23332  lmss  23507  fclsbas  24231  isfcf  24244  ucnima  24490  metcnp3  24750  cfilucfil  24769  bndth  25170  ellimc3  26091  lmxrge0  34408  gsumesum  34515  esumcst  34519  esumfsup  34526  voliune  34686  volfiniune  34687  bnj517  35340  nummin  35544  axprALT2  35563  onvf1odlem1  35646  fvineqsneq  38117  cover2  38426  naddgeoa  44181  prmunb2  45081