Theorem r19.29r 3126

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

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

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 3077  df-rex 3087

This theorem is used by:  r19.29imd  3127  2reu5  3716  rlimuni  15638  rlimno1  15742  neindisj2  23349  lmss  23524  fclsbas  24248  isfcf  24261  ucnima  24507  metcnp3  24767  cfilucfil  24786  bndth  25187  ellimc3  26107  lmxrge0  34463  gsumesum  34570  esumcst  34574  esumfsup  34581  voliune  34741  volfiniune  34742  bnj517  35395  nummin  35599  axprALT2  35618  onvf1odlem1  35701  fvineqsneq  38167  cover2  38466  naddgeoa  44236  prmunb2  45136