Theorem r19.29 3094

Description: Restricted quantifier version of 19.29 1873. See also r19.29r 3096. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 22-Dec-2024.)

Assertion

Ref	Expression
r19.29	⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Proof of Theorem r19.29

Step	Hyp	Ref	Expression
1		ibar 528	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3087	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpa 476	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3044  ∃wrex 3053

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  r19.29rOLD  3097  2r19.29  3119  disjiun  5090  triun  5224  ralxfrd  5358  ralxfrd2  5362  elrnmptg  5914  fmpt  7064  fliftfun  7269  fiunlem  7900  fiun  7901  f1iun  7902  omabs  8592  findcard3  9205  findcard3OLD  9206  r1sdom  9703  tcrank  9813  infxpenlem  9942  dfac12k  10077  cfslb2n  10197  cfcoflem  10201  iundom2g  10469  supsrlem  11040  axpre-sup  11098  fimaxre3  12105  hashgt23el  14365  limsupbnd2  15425  rlimuni  15492  rlimcld2  15520  rlimno1  15596  pgpfac1lem5  19987  rhmdvdsr  20393  ppttop  22870  epttop  22872  tgcnp  23116  lmcnp  23167  bwth  23273  1stcrest  23316  txlm  23511  tx1stc  23513  fbfinnfr  23704  fbunfip  23732  filuni  23748  ufileu  23782  fbflim2  23840  flftg  23859  ufilcmp  23895  cnpfcf  23904  tsmsxp  24018  metss  24372  lmmbr  25134  ivthlem2  25329  ivthlem3  25330  dyadmax  25475  tpr2rico  33875  esumpcvgval  34041  sigaclcuni  34081  voliune  34192  volfiniune  34193  dya2icoseg2  34242  onvf1odlem1  35063  umgr2cycllem  35100  umgr2cycl  35101  poimirlem29  37616  unirep  37681  heibor1lem  37776  pmapglbx  39736  stoweidlem35  46006