Theorem r19.29r 3100

Description: Restricted quantifier version of 19.29r 1875; variation of r19.29 3099. (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 3093	. 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 1796  ax-4 1810

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3052  df-rex 3061

This theorem is referenced by:  r19.29imd  3101  2reu5  3716  rlimuni  15473  rlimno1  15577  neindisj2  23067  lmss  23242  fclsbas  23965  isfcf  23978  ucnima  24224  metcnp3  24484  cfilucfil  24503  bndth  24913  ellimc3  25836  lmxrge0  34109  gsumesum  34216  esumcst  34220  esumfsup  34227  voliune  34386  volfiniune  34387  bnj517  35041  nummin  35249  onvf1odlem1  35297  fvineqsneq  37617  cover2  37916  naddgeoa  43636  prmunb2  44552