Theorem r19.29 3120

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3067  ∃wrex 3076

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-ral 3068  df-rex 3077

This theorem is referenced by:  r19.29rOLD  3123  2r19.29  3145  r19.29d2rOLD  3147  disjiun  5154  triun  5298  ralxfrd  5426  ralxfrd2  5430  elrnmptg  5984  fmpt  7144  fliftfun  7348  fiunlem  7982  fiun  7983  f1iun  7984  omabs  8707  findcard3  9346  findcard3OLD  9347  r1sdom  9843  tcrank  9953  infxpenlem  10082  dfac12k  10217  cfslb2n  10337  cfcoflem  10341  iundom2g  10609  supsrlem  11180  axpre-sup  11238  fimaxre3  12241  hashgt23el  14473  limsupbnd2  15529  rlimuni  15596  rlimcld2  15624  rlimno1  15702  pgpfac1lem5  20123  rhmdvdsr  20534  ppttop  23035  epttop  23037  tgcnp  23282  lmcnp  23333  bwth  23439  1stcrest  23482  txlm  23677  tx1stc  23679  fbfinnfr  23870  fbunfip  23898  filuni  23914  ufileu  23948  fbflim2  24006  flftg  24025  ufilcmp  24061  cnpfcf  24070  tsmsxp  24184  metss  24542  lmmbr  25311  ivthlem2  25506  ivthlem3  25507  dyadmax  25652  tpr2rico  33858  esumpcvgval  34042  sigaclcuni  34082  voliune  34193  volfiniune  34194  dya2icoseg2  34243  umgr2cycllem  35108  umgr2cycl  35109  poimirlem29  37609  unirep  37674  heibor1lem  37769  pmapglbx  39726  stoweidlem35  45956