Theorem r19.29 3183

Description: Restricted quantifier version of 19.29 1877. See also r19.29r 3184. (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 469	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
2	1	ralimi 3086	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)))
3		rexim 3168	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
4	2, 3	syl 17	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
5	4	imp 406	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3063  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  r19.29r  3184  2r19.29  3260  r19.29d2rOLD  3262  disjiun  5057  triun  5200  ralxfrd  5326  ralxfrd2  5330  elrnmptg  5857  fmpt  6966  fliftfun  7163  fiunlem  7758  fiun  7759  f1iun  7760  omabs  8441  findcard3  8987  r1sdom  9463  tcrank  9573  infxpenlem  9700  dfac12k  9834  cfslb2n  9955  cfcoflem  9959  iundom2g  10227  supsrlem  10798  axpre-sup  10856  fimaxre3  11851  hashgt23el  14067  limsupbnd2  15120  rlimuni  15187  rlimcld2  15215  rlimno1  15293  pgpfac1lem5  19597  ppttop  22065  epttop  22067  tgcnp  22312  lmcnp  22363  bwth  22469  1stcrest  22512  txlm  22707  tx1stc  22709  fbfinnfr  22900  fbunfip  22928  filuni  22944  ufileu  22978  fbflim2  23036  flftg  23055  ufilcmp  23091  cnpfcf  23100  tsmsxp  23214  metss  23570  lmmbr  24327  ivthlem2  24521  ivthlem3  24522  dyadmax  24667  rhmdvdsr  31419  tpr2rico  31764  esumpcvgval  31946  sigaclcuni  31986  voliune  32097  volfiniune  32098  dya2icoseg2  32145  umgr2cycllem  33002  umgr2cycl  33003  poimirlem29  35733  unirep  35798  heibor1lem  35894  pmapglbx  37710  stoweidlem35  43466