Theorem r19.29r 3116

Description: Restricted quantifier version of 19.29r 1877; variation of r19.29 3114. (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 528	. . 3 ⊢ (𝜓 → (𝜑 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3106	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpac 479	1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 396  ∀wral 3061  ∃wrex 3070

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-ral 3062  df-rex 3071

This theorem is referenced by:  r19.29imd  3118  2reu5  3754  rlimuni  15498  rlimno1  15604  neindisj2  22847  lmss  23022  fclsbas  23745  isfcf  23758  ucnima  24006  metcnp3  24269  cfilucfil  24288  bndth  24698  ellimc3  25620  lmxrge0  33218  gsumesum  33343  esumcst  33347  esumfsup  33354  voliune  33513  volfiniune  33514  bnj517  34182  nummin  34380  fvineqsneq  36596  cover2  36886  naddgeoa  42447  prmunb2  43372