Theorem r19.29r 3101

Description: Restricted quantifier version of 19.29r 1876; variation of r19.29 3100. (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 3061

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

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

This theorem is referenced by:  r19.29imd  3102  2reu5  3704  rlimuni  15512  rlimno1  15616  neindisj2  23088  lmss  23263  fclsbas  23986  isfcf  23999  ucnima  24245  metcnp3  24505  cfilucfil  24524  bndth  24925  ellimc3  25846  lmxrge0  34096  gsumesum  34203  esumcst  34207  esumfsup  34214  voliune  34373  volfiniune  34374  bnj517  35027  nummin  35236  axprALT2  35253  onvf1odlem1  35285  fvineqsneq  37728  cover2  38036  naddgeoa  43822  prmunb2  44738