Theorem r19.29r 3102

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3052  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053  df-rex 3063

This theorem is referenced by:  r19.29imd  3103  2reu5  3705  rlimuni  15506  rlimno1  15610  neindisj2  23101  lmss  23276  fclsbas  23999  isfcf  24012  ucnima  24258  metcnp3  24518  cfilucfil  24537  bndth  24938  ellimc3  25859  lmxrge0  34115  gsumesum  34222  esumcst  34226  esumfsup  34233  voliune  34392  volfiniune  34393  bnj517  35046  nummin  35255  axprALT2  35272  onvf1odlem1  35304  fvineqsneq  37745  cover2  38053  naddgeoa  43843  prmunb2  44759