Theorem r19.29 3094

Description: Restricted quantifier version of 19.29 1873. See also r19.29r 3096. (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 3087	. 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:  r19.29rOLD  3097  2r19.29  3119  disjiun  5090  triun  5224  ralxfrd  5358  ralxfrd2  5362  elrnmptg  5914  fmpt  7064  fliftfun  7269  fiunlem  7900  fiun  7901  f1iun  7902  omabs  8592  findcard3  9205  findcard3OLD  9206  r1sdom  9703  tcrank  9813  infxpenlem  9942  dfac12k  10077  cfslb2n  10197  cfcoflem  10201  iundom2g  10469  supsrlem  11040  axpre-sup  11098  fimaxre3  12105  hashgt23el  14365  limsupbnd2  15425  rlimuni  15492  rlimcld2  15520  rlimno1  15596  pgpfac1lem5  19995  rhmdvdsr  20428  ppttop  22927  epttop  22929  tgcnp  23173  lmcnp  23224  bwth  23330  1stcrest  23373  txlm  23568  tx1stc  23570  fbfinnfr  23761  fbunfip  23789  filuni  23805  ufileu  23839  fbflim2  23897  flftg  23916  ufilcmp  23952  cnpfcf  23961  tsmsxp  24075  metss  24429  lmmbr  25191  ivthlem2  25386  ivthlem3  25387  dyadmax  25532  tpr2rico  33895  esumpcvgval  34061  sigaclcuni  34101  voliune  34212  volfiniune  34213  dya2icoseg2  34262  onvf1odlem1  35083  umgr2cycllem  35120  umgr2cycl  35121  poimirlem29  37636  unirep  37701  heibor1lem  37796  pmapglbx  39756  stoweidlem35  46026