Theorem r19.29r 3113

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3058  ∃wrex 3067

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-ral 3059  df-rex 3068

This theorem is referenced by:  r19.29imd  3115  2reu5  3766  rlimuni  15582  rlimno1  15686  neindisj2  23146  lmss  23321  fclsbas  24044  isfcf  24057  ucnima  24305  metcnp3  24568  cfilucfil  24587  bndth  25003  ellimc3  25928  lmxrge0  33912  gsumesum  34039  esumcst  34043  esumfsup  34050  voliune  34209  volfiniune  34210  bnj517  34877  nummin  35083  fvineqsneq  37394  cover2  37701  naddgeoa  43383  prmunb2  44306