Theorem r19.29 3184

Description: Restricted quantifier version of 19.29 1876. See also r19.29r 3185. (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 470	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
2	1	ralimi 3087	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)))
3		rexim 3172	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
4	2, 3	syl 17	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
5	4	imp 407	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 396  ∀wral 3064  ∃wrex 3065

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  r19.29r  3185  2r19.29  3263  r19.29d2rOLD  3265  disjiun  5061  triun  5204  ralxfrd  5331  ralxfrd2  5335  elrnmptg  5868  fmpt  6984  fliftfun  7183  fiunlem  7784  fiun  7785  f1iun  7786  omabs  8481  findcard3  9057  r1sdom  9532  tcrank  9642  infxpenlem  9769  dfac12k  9903  cfslb2n  10024  cfcoflem  10028  iundom2g  10296  supsrlem  10867  axpre-sup  10925  fimaxre3  11921  hashgt23el  14139  limsupbnd2  15192  rlimuni  15259  rlimcld2  15287  rlimno1  15365  pgpfac1lem5  19682  ppttop  22157  epttop  22159  tgcnp  22404  lmcnp  22455  bwth  22561  1stcrest  22604  txlm  22799  tx1stc  22801  fbfinnfr  22992  fbunfip  23020  filuni  23036  ufileu  23070  fbflim2  23128  flftg  23147  ufilcmp  23183  cnpfcf  23192  tsmsxp  23306  metss  23664  lmmbr  24422  ivthlem2  24616  ivthlem3  24617  dyadmax  24762  rhmdvdsr  31517  tpr2rico  31862  esumpcvgval  32046  sigaclcuni  32086  voliune  32197  volfiniune  32198  dya2icoseg2  32245  umgr2cycllem  33102  umgr2cycl  33103  poimirlem29  35806  unirep  35871  heibor1lem  35967  pmapglbx  37783  stoweidlem35  43576