Theorem r19.29 3092

Description: Restricted quantifier version of 19.29 1873. See also r19.29r 3093. (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 3086	. 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:  2r19.29  3115  disjiun  5080  triun  5213  ralxfrd  5347  ralxfrd2  5351  elrnmptg  5903  fmpt  7044  fliftfun  7249  fiunlem  7877  fiun  7878  f1iun  7879  omabs  8569  findcard3  9172  r1sdom  9670  tcrank  9780  infxpenlem  9907  dfac12k  10042  cfslb2n  10162  cfcoflem  10166  iundom2g  10434  supsrlem  11005  axpre-sup  11063  fimaxre3  12071  hashgt23el  14331  limsupbnd2  15390  rlimuni  15457  rlimcld2  15485  rlimno1  15561  pgpfac1lem5  19960  rhmdvdsr  20393  ppttop  22892  epttop  22894  tgcnp  23138  lmcnp  23189  bwth  23295  1stcrest  23338  txlm  23533  tx1stc  23535  fbfinnfr  23726  fbunfip  23754  filuni  23770  ufileu  23804  fbflim2  23862  flftg  23881  ufilcmp  23917  cnpfcf  23926  tsmsxp  24040  metss  24394  lmmbr  25156  ivthlem2  25351  ivthlem3  25352  dyadmax  25497  tpr2rico  33879  esumpcvgval  34045  sigaclcuni  34085  voliune  34196  volfiniune  34197  dya2icoseg2  34246  onvf1odlem1  35076  umgr2cycllem  35113  umgr2cycl  35114  poimirlem29  37629  unirep  37694  heibor1lem  37789  pmapglbx  39748  stoweidlem35  46016