Theorem r19.29 3101

Description: Restricted quantifier version of 19.29 1841. See also r19.29r 3102. (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 462	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
2	1	ralimi 2981	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)))
3		rexim 3037	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
4	2, 3	syl 17	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
5	4	imp 444	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 383  ∀wral 2941  ∃wrex 2942

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

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947

This theorem is referenced by:  r19.29r  3102  2r19.29  3108  r19.29d2r  3109  disjiun  4672  triun  4799  ralxfrd  4909  ralxfrdOLD  4910  ralxfrd2  4914  elrnmptg  5407  fmpt  6421  fliftfun  6602  fun11iun  7168  omabs  7772  findcard3  8244  r1sdom  8675  tcrank  8785  infxpenlem  8874  dfac12k  9007  cfslb2n  9128  cfcoflem  9132  iundom2g  9400  supsrlem  9970  axpre-sup  10028  fimaxre3  11008  limsupbnd2  14258  rlimuni  14325  rlimcld2  14353  rlimno1  14428  pgpfac1lem5  18524  ppttop  20859  epttop  20861  tgcnp  21105  lmcnp  21156  bwth  21261  1stcrest  21304  txlm  21499  tx1stc  21501  fbfinnfr  21692  fbunfip  21720  filuni  21736  ufileu  21770  fbflim2  21828  flftg  21847  ufilcmp  21883  cnpfcf  21892  tsmsxp  22005  metss  22360  lmmbr  23102  ivthlem2  23267  ivthlem3  23268  dyadmax  23412  rhmdvdsr  29946  tpr2rico  30086  esumpcvgval  30268  sigaclcuni  30309  voliune  30420  volfiniune  30421  dya2icoseg2  30468  poimirlem29  33568  unirep  33637  heibor1lem  33738  pmapglbx  35373  stoweidlem35  40570