Theorem r19.29r 3130

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

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

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 3081  df-rex 3091

This theorem is used by:  r19.29imd  3131  2reu5  3719  rlimuni  15761  rlimno1  15865  neindisj2  23496  lmss  23671  fclsbas  24395  isfcf  24408  ucnima  24654  metcnp3  24914  cfilucfil  24933  bndth  25334  ellimc3  26254  lmxrge0  34695  gsumesum  34802  esumcst  34806  esumfsup  34813  voliune  34973  volfiniune  34974  bnj517  35626  nummin  35847  axprALT2  35857  onvf1odlem1  36072  fvineqsneq  38603  cover2  38917  naddgeoa  44657  prmunb2  45556