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 529	. . 3 ⊢ (𝜓 → (𝜑 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3106	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpac 480	1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 397  ∀wral 3062  ∃wrex 3071

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 398  df-ex 1782  df-ral 3063  df-rex 3072

This theorem is referenced by:  r19.29imd  3118  2reu5  3708  rlimuni  15359  rlimno1  15465  neindisj2  22380  lmss  22555  fclsbas  23278  isfcf  23291  ucnima  23539  metcnp3  23802  cfilucfil  23821  bndth  24227  ellimc3  25149  lmxrge0  32198  gsumesum  32323  esumcst  32327  esumfsup  32334  voliune  32493  volfiniune  32494  bnj517  33162  nummin  33360  fvineqsneq  35737  cover2  36026  prmunb2  42300