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  3718  rlimuni  15485  rlimno1  15589  neindisj2  23079  lmss  23254  fclsbas  23977  isfcf  23990  ucnima  24236  metcnp3  24496  cfilucfil  24515  bndth  24925  ellimc3  25848  lmxrge0  34130  gsumesum  34237  esumcst  34241  esumfsup  34248  voliune  34407  volfiniune  34408  bnj517  35061  nummin  35270  axprALT2  35287  onvf1odlem1  35319  fvineqsneq  37667  cover2  37966  naddgeoa  43751  prmunb2  44667