Theorem r19.29 3115

Description: Restricted quantifier version of 19.29 1877. See also r19.29r 3117. (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 530	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3107	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpa 478	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 397  ∀wral 3062  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3063  df-rex 3072

This theorem is referenced by:  r19.29rOLD  3118  2r19.29  3140  r19.29d2rOLD  3142  disjiun  5136  triun  5281  ralxfrd  5407  ralxfrd2  5411  elrnmptg  5959  fmpt  7110  fliftfun  7309  fiunlem  7928  fiun  7929  f1iun  7930  omabs  8650  findcard3  9285  findcard3OLD  9286  r1sdom  9769  tcrank  9879  infxpenlem  10008  dfac12k  10142  cfslb2n  10263  cfcoflem  10267  iundom2g  10535  supsrlem  11106  axpre-sup  11164  fimaxre3  12160  hashgt23el  14384  limsupbnd2  15427  rlimuni  15494  rlimcld2  15522  rlimno1  15600  pgpfac1lem5  19949  rhmdvdsr  20287  ppttop  22510  epttop  22512  tgcnp  22757  lmcnp  22808  bwth  22914  1stcrest  22957  txlm  23152  tx1stc  23154  fbfinnfr  23345  fbunfip  23373  filuni  23389  ufileu  23423  fbflim2  23481  flftg  23500  ufilcmp  23536  cnpfcf  23545  tsmsxp  23659  metss  24017  lmmbr  24775  ivthlem2  24969  ivthlem3  24970  dyadmax  25115  tpr2rico  32892  esumpcvgval  33076  sigaclcuni  33116  voliune  33227  volfiniune  33228  dya2icoseg2  33277  umgr2cycllem  34131  umgr2cycl  34132  poimirlem29  36517  unirep  36582  heibor1lem  36677  pmapglbx  38640  stoweidlem35  44751