Theorem r19.29 3254

Description: Restricted quantifier version of 19.29 1874. See also r19.29r 3255. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Assertion

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

Proof of Theorem r19.29

Step	Hyp	Ref	Expression
1		pm3.2 472	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
2	1	ralimi 3160	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)))
3		rexim 3241	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
4	2, 3	syl 17	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
5	4	imp 409	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 398  ∀wral 3138  ∃wrex 3139

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3143  df-rex 3144

This theorem is referenced by:  r19.29r  3255  r19.29rOLD  3256  2r19.29  3334  r19.29d2r  3335  disjiun  5053  triun  5185  ralxfrd  5309  ralxfrd2  5313  elrnmptg  5831  fmpt  6874  fliftfun  7065  fiunlem  7643  fiun  7644  f1iun  7645  omabs  8274  findcard3  8761  r1sdom  9203  tcrank  9313  infxpenlem  9439  dfac12k  9573  cfslb2n  9690  cfcoflem  9694  iundom2g  9962  supsrlem  10533  axpre-sup  10591  fimaxre3  11587  hashgt23el  13786  limsupbnd2  14840  rlimuni  14907  rlimcld2  14935  rlimno1  15010  pgpfac1lem5  19201  ppttop  21615  epttop  21617  tgcnp  21861  lmcnp  21912  bwth  22018  1stcrest  22061  txlm  22256  tx1stc  22258  fbfinnfr  22449  fbunfip  22477  filuni  22493  ufileu  22527  fbflim2  22585  flftg  22604  ufilcmp  22640  cnpfcf  22649  tsmsxp  22763  metss  23118  lmmbr  23861  ivthlem2  24053  ivthlem3  24054  dyadmax  24199  rhmdvdsr  30891  tpr2rico  31155  esumpcvgval  31337  sigaclcuni  31377  voliune  31488  volfiniune  31489  dya2icoseg2  31536  umgr2cycllem  32387  umgr2cycl  32388  poimirlem29  34936  unirep  35003  heibor1lem  35102  pmapglbx  36920  stoweidlem35  42340