Theorem r19.29 3097

Description: Restricted quantifier version of 19.29 1874. See also r19.29r 3098. (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 3091	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpa 476	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3049  ∃wrex 3058

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3050  df-rex 3059

This theorem is referenced by:  2r19.29  3120  disjiun  5084  triun  5217  ralxfrd  5351  ralxfrd2  5355  elrnmptg  5908  fmpt  7053  fliftfun  7256  fiunlem  7884  fiun  7885  f1iun  7886  omabs  8577  findcard3  9181  r1sdom  9684  tcrank  9794  infxpenlem  9921  dfac12k  10056  cfslb2n  10176  cfcoflem  10180  iundom2g  10448  supsrlem  11020  axpre-sup  11078  fimaxre3  12086  hashgt23el  14345  limsupbnd2  15404  rlimuni  15471  rlimcld2  15499  rlimno1  15575  pgpfac1lem5  20008  rhmdvdsr  20439  ppttop  22949  epttop  22951  tgcnp  23195  lmcnp  23246  bwth  23352  1stcrest  23395  txlm  23590  tx1stc  23592  fbfinnfr  23783  fbunfip  23811  filuni  23827  ufileu  23861  fbflim2  23919  flftg  23938  ufilcmp  23974  cnpfcf  23983  tsmsxp  24097  metss  24450  lmmbr  25212  ivthlem2  25407  ivthlem3  25408  dyadmax  25553  tpr2rico  34018  esumpcvgval  34184  sigaclcuni  34224  voliune  34335  volfiniune  34336  dya2icoseg2  34384  onvf1odlem1  35246  umgr2cycllem  35283  umgr2cycl  35284  poimirlem29  37789  unirep  37854  heibor1lem  37949  pmapglbx  39968  stoweidlem35  46221