Theorem r19.29r 3103

Description: Restricted quantifier version of 19.29r 1881; variation of r19.29 3102. (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 532	. . 3 ⊢ (𝜓 → (𝜑 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3096	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpac 479	1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 396  ∀wral 3053  ∃wrex 3063

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3054  df-rex 3064

This theorem is referenced by:  r19.29imd  3104  2reu5  3699  rlimuni  15503  rlimno1  15607  neindisj2  23106  lmss  23281  fclsbas  24004  isfcf  24017  ucnima  24263  metcnp3  24523  cfilucfil  24542  bndth  24943  ellimc3  25864  lmxrge0  34136  gsumesum  34243  esumcst  34247  esumfsup  34254  voliune  34413  volfiniune  34414  bnj517  35067  nummin  35274  axprALT2  35290  onvf1odlem1  35331  fvineqsneq  37774  cover2  38082  naddgeoa  43839  prmunb2  44755