Theorem r19.29r 3103

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3051  ∃wrex 3060

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 3052  df-rex 3061

This theorem is referenced by:  r19.29imd  3105  2reu5  3741  rlimuni  15566  rlimno1  15670  neindisj2  23061  lmss  23236  fclsbas  23959  isfcf  23972  ucnima  24219  metcnp3  24479  cfilucfil  24498  bndth  24908  ellimc3  25832  lmxrge0  33983  gsumesum  34090  esumcst  34094  esumfsup  34101  voliune  34260  volfiniune  34261  bnj517  34916  nummin  35122  fvineqsneq  37430  cover2  37739  naddgeoa  43418  prmunb2  44335