Theorem r19.29 3257

Description: Restricted quantifier version of 19.29 1873. See also r19.29r 3258. (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 3163	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)))
3		rexim 3244	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
4	2, 3	syl 17	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
5	4	imp 409	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 398  ∀wral 3141  ∃wrex 3142

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-ral 3146  df-rex 3147

This theorem is referenced by:  r19.29r  3258  r19.29rOLD  3259  2r19.29  3337  r19.29d2r  3338  disjiun  5056  triun  5188  ralxfrd  5312  ralxfrd2  5316  elrnmptg  5834  fmpt  6877  fliftfun  7068  fiunlem  7646  fiun  7647  f1iun  7648  omabs  8277  findcard3  8764  r1sdom  9206  tcrank  9316  infxpenlem  9442  dfac12k  9576  cfslb2n  9693  cfcoflem  9697  iundom2g  9965  supsrlem  10536  axpre-sup  10594  fimaxre3  11590  hashgt23el  13788  limsupbnd2  14843  rlimuni  14910  rlimcld2  14938  rlimno1  15013  pgpfac1lem5  19204  ppttop  21618  epttop  21620  tgcnp  21864  lmcnp  21915  bwth  22021  1stcrest  22064  txlm  22259  tx1stc  22261  fbfinnfr  22452  fbunfip  22480  filuni  22496  ufileu  22530  fbflim2  22588  flftg  22607  ufilcmp  22643  cnpfcf  22652  tsmsxp  22766  metss  23121  lmmbr  23864  ivthlem2  24056  ivthlem3  24057  dyadmax  24202  rhmdvdsr  30895  tpr2rico  31159  esumpcvgval  31341  sigaclcuni  31381  voliune  31492  volfiniune  31493  dya2icoseg2  31540  umgr2cycllem  32391  umgr2cycl  32392  poimirlem29  34925  unirep  34992  heibor1lem  35091  pmapglbx  36909  stoweidlem35  42327