Theorem r19.29r 3126

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

Syntax hints:   → wi 4   ∧ wa 399  ∀wral 3076  ∃wrex 3086

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-ral 3077  df-rex 3087

This theorem is referenced by:  r19.29imd  3127  2reu5  3721  rlimuni  15577  rlimno1  15681  neindisj2  23183  lmss  23358  fclsbas  24081  isfcf  24094  ucnima  24340  metcnp3  24600  cfilucfil  24619  bndth  25020  ellimc3  25941  lmxrge0  34249  gsumesum  34356  esumcst  34360  esumfsup  34367  voliune  34526  volfiniune  34527  bnj517  35180  nummin  35389  axprALT2  35405  onvf1odlem1  35446  fvineqsneq  37906  cover2  38214  naddgeoa  43971  prmunb2  44887