Theorem r19.29 3128

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

Syntax hints:   → wi 4   ∧ wa 400  ∀wral 3079  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080  df-rex 3090

This theorem is referenced by:  2r19.29  3151  disjiun  5097  triun  5233  ralxfrd  5379  ralxfrd2  5383  elrnmptg  5951  fmpt  7105  fliftfun  7310  fiunlem  7935  fiun  7936  f1iun  7937  omabs  8633  findcard3  9239  r1sdom  9742  tcrank  9852  infxpenlem  9993  dfac12k  10127  cfslb2n  10247  cfcoflem  10251  iundom2g  10519  supsrlem  11091  axpre-sup  11149  fimaxre3  12156  hashgt23el  14457  limsupbnd2  15530  rlimuni  15597  rlimcld2  15625  rlimno1  15701  pgpfac1lem5  20146  rhmdvdsr  20605  ppttop  23164  epttop  23166  tgcnp  23410  lmcnp  23461  bwth  23567  1stcrest  23610  txlm  23805  tx1stc  23807  fbfinnfr  23998  fbunfip  24026  filuni  24042  ufileu  24076  fbflim2  24134  flftg  24153  ufilcmp  24189  cnpfcf  24198  tsmsxp  24312  metss  24665  lmmbr  25417  ivthlem2  25611  ivthlem3  25612  dyadmax  25757  tpr2rico  34302  esumpcvgval  34468  sigaclcuni  34508  voliune  34619  volfiniune  34620  dya2icoseg2  34668  onvf1odlem1  35587  umgr2cycllem  35632  umgr2cycl  35633  poimirlem29  38300  unirep  38365  heibor1lem  38460  pmapglbx  40543  stoweidlem35  46749