Theorem r19.29r 3211

Description: Restricted quantifier version of 19.29r 1951; variation of r19.29 3210. (Contributed by NM, 31-Aug-1999.)

Assertion

Ref	Expression
r19.29r	⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Proof of Theorem r19.29r

Step	Hyp	Ref	Expression
1		r19.29 3210	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜓 ∧ ∃𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
2		ancom 465	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜓 ∧ ∃𝑥 ∈ 𝐴 𝜑))
3		ancom 465	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
4	3	rexbii 3179	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
5	1, 2, 4	3imtr4i 281	1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 383  ∀wral 3050  ∃wrex 3051

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

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-ral 3055  df-rex 3056

This theorem is referenced by:  r19.29imd  3212  2reu5  3557  rlimuni  14480  rlimno1  14583  neindisj2  21129  lmss  21304  fclsbas  22026  isfcf  22039  ucnima  22286  metcnp3  22546  cfilucfil  22565  bndth  22958  ellimc3  23842  lmxrge0  30307  gsumesum  30430  esumcst  30434  esumfsup  30441  voliune  30601  volfiniune  30602  bnj517  31262  cover2  33821  prmunb2  39012