Theorem r19.29r 3105

Description: Restricted quantifier version of 19.29r 1882; variation of r19.29 3104. (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 533	. . 3 ⊢ (𝜓 → (𝜑 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3098	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpac 480	1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 397  ∀wral 3055  ∃wrex 3065

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

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-ral 3056  df-rex 3066

This theorem is referenced by:  r19.29imd  3106  2reu5  3700  rlimuni  15507  rlimno1  15611  neindisj2  23109  lmss  23284  fclsbas  24007  isfcf  24020  ucnima  24266  metcnp3  24526  cfilucfil  24545  bndth  24946  ellimc3  25867  lmxrge0  34146  gsumesum  34253  esumcst  34257  esumfsup  34264  voliune  34423  volfiniune  34424  bnj517  35080  nummin  35287  axprALT2  35303  onvf1odlem1  35344  fvineqsneq  37787  cover2  38095  naddgeoa  43852  prmunb2  44768