Theorem r19.29r 3117

Description: Restricted quantifier version of 19.29r 1878; variation of r19.29 3115. (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 529	. . 3 ⊢ (𝜓 → (𝜑 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3107	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpac 480	1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 397  ∀wral 3062  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3063  df-rex 3072

This theorem is referenced by:  r19.29imd  3119  2reu5  3755  rlimuni  15494  rlimno1  15600  neindisj2  22627  lmss  22802  fclsbas  23525  isfcf  23538  ucnima  23786  metcnp3  24049  cfilucfil  24068  bndth  24474  ellimc3  25396  lmxrge0  32932  gsumesum  33057  esumcst  33061  esumfsup  33068  voliune  33227  volfiniune  33228  bnj517  33896  nummin  34094  fvineqsneq  36293  cover2  36583  naddgeoa  42145  prmunb2  43070