Theorem r19.29 3282

Description: Restricted quantifier version of 19.29 1976. See also r19.29r 3283. (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 463	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
2	1	ralimi 3161	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)))
3		rexim 3216	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
4	2, 3	syl 17	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
5	4	imp 397	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 386  ∀wral 3117  ∃wrex 3118

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

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-ral 3122  df-rex 3123

This theorem is referenced by:  r19.29r  3283  2r19.29  3289  r19.29d2r  3290  disjiun  4863  triun  4990  ralxfrd  5110  ralxfrd2  5114  elrnmptg  5612  fmpt  6634  fliftfun  6822  fun11iun  7393  omabs  7999  findcard3  8478  r1sdom  8921  tcrank  9031  infxpenlem  9156  dfac12k  9291  cfslb2n  9412  cfcoflem  9416  iundom2g  9684  supsrlem  10255  axpre-sup  10313  fimaxre3  11307  limsupbnd2  14598  rlimuni  14665  rlimcld2  14693  rlimno1  14768  pgpfac1lem5  18839  ppttop  21189  epttop  21191  tgcnp  21435  lmcnp  21486  bwth  21591  1stcrest  21634  txlm  21829  tx1stc  21831  fbfinnfr  22022  fbunfip  22050  filuni  22066  ufileu  22100  fbflim2  22158  flftg  22177  ufilcmp  22213  cnpfcf  22222  tsmsxp  22335  metss  22690  lmmbr  23433  ivthlem2  23625  ivthlem3  23626  dyadmax  23771  rhmdvdsr  30359  tpr2rico  30499  esumpcvgval  30681  sigaclcuni  30722  voliune  30833  volfiniune  30834  dya2icoseg2  30881  poimirlem29  33977  unirep  34045  heibor1lem  34145  pmapglbx  35839  stoweidlem35  41040