Theorem r19.29 3129

Description: Restricted quantifier version of 19.29 1908. See also r19.29r 3130. (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 538	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3123	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpa 482	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wral 3080  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3081  df-rex 3091

This theorem is used by:  2r19.29  3152  disjiun  5096  triun  5233  ralxfrd  5377  ralxfrd2  5381  elrnmptg  5955  fmpt  7142  fliftfun  7351  fiunlem  7988  fiun  7989  f1iun  7990  omabs  8698  findcard3  9312  r1sdom  9818  tcrank  9938  infxpenlem  10131  dfac12k  10265  cfslb2n  10385  cfcoflem  10389  iundom2g  10663  supsrlem  11235  axpre-sup  11293  fimaxre3  12303  hashgt23el  14610  limsupbnd2  15694  rlimuni  15761  rlimcld2  15789  rlimno1  15865  pgpfac1lem5  20346  rhmdvdsr  20809  ppttop  23380  epttop  23382  tgcnp  23626  lmcnp  23677  bwth  23783  1stcrest  23826  txlm  24022  tx1stc  24024  fbfinnfr  24215  fbunfip  24243  filuni  24259  ufileu  24293  fbflim2  24351  flftg  24370  ufilcmp  24406  cnpfcf  24415  tsmsxp  24529  metss  24882  lmmbr  25634  ivthlem2  25828  ivthlem3  25829  dyadmax  25974  umgr2cycllem  30803  umgr2cycl  30804  tpr2rico  34655  esumpcvgval  34821  sigaclcuni  34861  voliune  34973  volfiniune  34974  dya2icoseg2  35021  onvf1odlem1  36072  poimirlem29  38835  unirep  38916  heibor1lem  39009  pmapglbx  41092  stoweidlem35  47318