Theorem r19.29r 3096

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3044  ∃wrex 3053

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  r19.29imd  3098  2reu5  3729  rlimuni  15516  rlimno1  15620  neindisj2  23010  lmss  23185  fclsbas  23908  isfcf  23921  ucnima  24168  metcnp3  24428  cfilucfil  24447  bndth  24857  ellimc3  25780  lmxrge0  33942  gsumesum  34049  esumcst  34053  esumfsup  34060  voliune  34219  volfiniune  34220  bnj517  34875  nummin  35081  onvf1odlem1  35090  fvineqsneq  37400  cover2  37709  naddgeoa  43383  prmunb2  44300