Theorem r19.29r 3129

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

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

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-ral 3080  df-rex 3090

This theorem is used by:  r19.29imd  3130  2reu5  3718  rlimuni  15729  rlimno1  15833  neindisj2  23453  lmss  23628  fclsbas  24352  isfcf  24365  ucnima  24611  metcnp3  24871  cfilucfil  24890  bndth  25291  ellimc3  26211  lmxrge0  34637  gsumesum  34744  esumcst  34748  esumfsup  34755  voliune  34915  volfiniune  34916  bnj517  35568  nummin  35783  axprALT2  35795  onvf1odlem1  35985  fvineqsneq  38475  cover2  38789  naddgeoa  44536  prmunb2  45435