Theorem r19.29r 3093

Description: Restricted quantifier version of 19.29r 1874; variation of r19.29 3092. (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 3086	. 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  3094  2reu5  3720  rlimuni  15476  rlimno1  15580  neindisj2  23027  lmss  23202  fclsbas  23925  isfcf  23938  ucnima  24185  metcnp3  24445  cfilucfil  24464  bndth  24874  ellimc3  25797  lmxrge0  33938  gsumesum  34045  esumcst  34049  esumfsup  34056  voliune  34215  volfiniune  34216  bnj517  34871  nummin  35077  onvf1odlem1  35095  fvineqsneq  37405  cover2  37714  naddgeoa  43387  prmunb2  44304