Theorem r19.29r 3135

Description: Restricted quantifier version of 19.29r 1901; variation of r19.29 3134. (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 536	. . 3 ⊢ (𝜓 → (𝜑 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3128	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpac 483	1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 400  ∀wral 3085  ∃wrex 3095

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-ral 3086  df-rex 3096

This theorem is referenced by:  r19.29imd  3136  2reu5  3730  rlimuni  15601  rlimno1  15705  neindisj2  23249  lmss  23424  fclsbas  24147  isfcf  24160  ucnima  24406  metcnp3  24666  cfilucfil  24685  bndth  25086  ellimc3  26007  lmxrge0  34287  gsumesum  34394  esumcst  34398  esumfsup  34405  voliune  34564  volfiniune  34565  bnj517  35218  nummin  35427  axprALT2  35445  onvf1odlem1  35486  fvineqsneq  37946  cover2  38254  naddgeoa  44013  prmunb2  44913