Theorem r19.29 3072

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

Syntax hints:   → wi 4   ∧ wa 384  ∀wral 2912  ∃wrex 2913

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

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  r19.29r  3073  2r19.29  3079  r19.29d2r  3080  disjiun  4640  triun  4766  ralxfrd  4879  ralxfrdOLD  4880  ralxfrd2  4884  elrnmptg  5375  fmpt  6381  fliftfun  6562  fun11iun  7126  omabs  7727  findcard3  8203  r1sdom  8637  tcrank  8747  infxpenlem  8836  dfac12k  8969  cfslb2n  9090  cfcoflem  9094  iundom2g  9362  supsrlem  9932  axpre-sup  9990  fimaxre3  10970  limsupbnd2  14214  rlimuni  14281  rlimcld2  14309  rlimno1  14384  pgpfac1lem5  18478  ppttop  20811  epttop  20813  tgcnp  21057  lmcnp  21108  bwth  21213  1stcrest  21256  txlm  21451  tx1stc  21453  fbfinnfr  21645  fbunfip  21673  filuni  21689  ufileu  21723  fbflim2  21781  flftg  21800  ufilcmp  21836  cnpfcf  21845  tsmsxp  21958  metss  22313  lmmbr  23056  ivthlem2  23221  ivthlem3  23222  dyadmax  23366  rhmdvdsr  29818  tpr2rico  29958  esumpcvgval  30140  sigaclcuni  30181  voliune  30292  volfiniune  30293  dya2icoseg2  30340  poimirlem29  33438  unirep  33507  heibor1lem  33608  pmapglbx  35055  stoweidlem35  40252