Theorem r19.29r 3129

Description: Restricted quantifier version of 19.29r 1904; variation of r19.29 3128. (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 536	. . 3 ⊢ (𝜓 → (𝜑 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3122	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpac 483	1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 400  ∀wral 3079  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080  df-rex 3090

This theorem is referenced by:  r19.29imd  3130  2reu5  3721  rlimuni  15597  rlimno1  15701  neindisj2  23280  lmss  23455  fclsbas  24178  isfcf  24191  ucnima  24437  metcnp3  24697  cfilucfil  24716  bndth  25117  ellimc3  26038  lmxrge0  34342  gsumesum  34449  esumcst  34453  esumfsup  34460  voliune  34619  volfiniune  34620  bnj517  35273  nummin  35484  axprALT2  35503  onvf1odlem1  35587  fvineqsneq  38078  cover2  38386  naddgeoa  44141  prmunb2  45041