Theorem r19.29 3130

Description: Restricted quantifier version of 19.29 1906. See also r19.29r 3131. (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 538	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3124	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpa 482	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wral 3081  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3082  df-rex 3092

This theorem is used by:  2r19.29  3153  disjiun  5099  triun  5235  ralxfrd  5381  ralxfrd2  5385  elrnmptg  5953  fmpt  7109  fliftfun  7319  fiunlem  7945  fiun  7946  f1iun  7947  omabs  8643  findcard3  9250  r1sdom  9753  tcrank  9863  infxpenlem  10013  dfac12k  10147  cfslb2n  10267  cfcoflem  10271  iundom2g  10539  supsrlem  11111  axpre-sup  11169  fimaxre3  12176  hashgt23el  14479  limsupbnd2  15558  rlimuni  15625  rlimcld2  15653  rlimno1  15729  pgpfac1lem5  20195  rhmdvdsr  20655  ppttop  23214  epttop  23216  tgcnp  23460  lmcnp  23511  bwth  23617  1stcrest  23660  txlm  23856  tx1stc  23858  fbfinnfr  24049  fbunfip  24077  filuni  24093  ufileu  24127  fbflim2  24185  flftg  24204  ufilcmp  24240  cnpfcf  24249  tsmsxp  24363  metss  24716  lmmbr  25468  ivthlem2  25662  ivthlem3  25663  dyadmax  25808  umgr2cycllem  30573  umgr2cycl  30574  tpr2rico  34366  esumpcvgval  34532  sigaclcuni  34572  voliune  34684  volfiniune  34685  dya2icoseg2  34733  onvf1odlem1  35644  poimirlem29  38357  unirep  38423  heibor1lem  38518  pmapglbx  40601  stoweidlem35  46807