Theorem r19.29 3099

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3051  ∃wrex 3060

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 3052  df-rex 3061

This theorem is referenced by:  2r19.29  3122  disjiun  5086  triun  5219  ralxfrd  5353  ralxfrd2  5357  elrnmptg  5910  fmpt  7055  fliftfun  7258  fiunlem  7886  fiun  7887  f1iun  7888  omabs  8579  findcard3  9183  r1sdom  9686  tcrank  9796  infxpenlem  9923  dfac12k  10058  cfslb2n  10178  cfcoflem  10182  iundom2g  10450  supsrlem  11022  axpre-sup  11080  fimaxre3  12088  hashgt23el  14347  limsupbnd2  15406  rlimuni  15473  rlimcld2  15501  rlimno1  15577  pgpfac1lem5  20010  rhmdvdsr  20441  ppttop  22951  epttop  22953  tgcnp  23197  lmcnp  23248  bwth  23354  1stcrest  23397  txlm  23592  tx1stc  23594  fbfinnfr  23785  fbunfip  23813  filuni  23829  ufileu  23863  fbflim2  23921  flftg  23940  ufilcmp  23976  cnpfcf  23985  tsmsxp  24099  metss  24452  lmmbr  25214  ivthlem2  25409  ivthlem3  25410  dyadmax  25555  tpr2rico  34069  esumpcvgval  34235  sigaclcuni  34275  voliune  34386  volfiniune  34387  dya2icoseg2  34435  onvf1odlem1  35297  umgr2cycllem  35334  umgr2cycl  35335  poimirlem29  37850  unirep  37915  heibor1lem  38010  pmapglbx  40029  stoweidlem35  46279