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  5131  triun  5276  ralxfrd  5402  ralxfrd2  5406  elrnmptg  5953  fmpt  7097  fliftfun  7296  fiunlem  7915  fiun  7916  f1iun  7917  omabs  8638  findcard3  9273  findcard3OLD  9274  r1sdom  9756  tcrank  9866  infxpenlem  9995  dfac12k  10129  cfslb2n  10250  cfcoflem  10254  iundom2g  10522  supsrlem  11093  axpre-sup  11151  fimaxre3  12147  hashgt23el  14371  limsupbnd2  15414  rlimuni  15481  rlimcld2  15509  rlimno1  15587  pgpfac1lem5  19932  rhmdvdsr  20265  ppttop  22479  epttop  22481  tgcnp  22726  lmcnp  22777  bwth  22883  1stcrest  22926  txlm  23121  tx1stc  23123  fbfinnfr  23314  fbunfip  23342  filuni  23358  ufileu  23392  fbflim2  23450  flftg  23469  ufilcmp  23505  cnpfcf  23514  tsmsxp  23628  metss  23986  lmmbr  24744  ivthlem2  24938  ivthlem3  24939  dyadmax  25084  tpr2rico  32823  esumpcvgval  33007  sigaclcuni  33047  voliune  33158  volfiniune  33159  dya2icoseg2  33208  umgr2cycllem  34062  umgr2cycl  34063  poimirlem29  36422  unirep  36487  heibor1lem  36583  pmapglbx  38546  stoweidlem35  44624