Theorem r19.29r 3097

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3045  ∃wrex 3054

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 3046  df-rex 3055

This theorem is referenced by:  r19.29imd  3099  2reu5  3732  rlimuni  15523  rlimno1  15627  neindisj2  23017  lmss  23192  fclsbas  23915  isfcf  23928  ucnima  24175  metcnp3  24435  cfilucfil  24454  bndth  24864  ellimc3  25787  lmxrge0  33949  gsumesum  34056  esumcst  34060  esumfsup  34067  voliune  34226  volfiniune  34227  bnj517  34882  nummin  35088  onvf1odlem1  35097  fvineqsneq  37407  cover2  37716  naddgeoa  43390  prmunb2  44307