Theorem r19.29r 3127

Description: Restricted quantifier version of 19.29r 1907; variation of r19.29 3126. (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 537	. . 3 ⊢ (𝜓 → (𝜑 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3120	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpac 484	1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wral 3077  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3078  df-rex 3088

This theorem is used by:  r19.29imd  3128  2reu5  3716  rlimuni  15717  rlimno1  15821  neindisj2  23441  lmss  23616  fclsbas  24340  isfcf  24353  ucnima  24599  metcnp3  24859  cfilucfil  24878  bndth  25279  ellimc3  26199  lmxrge0  34584  gsumesum  34691  esumcst  34695  esumfsup  34702  voliune  34862  volfiniune  34863  bnj517  35515  nummin  35722  axprALT2  35734  onvf1odlem1  35882  fvineqsneq  38335  cover2  38649  naddgeoa  44395  prmunb2  45294