Theorem r19.29 3095

Description: Restricted quantifier version of 19.29 1874. 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 3089	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpa 476	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3047  ∃wrex 3056

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3048  df-rex 3057

This theorem is referenced by:  2r19.29  3118  disjiun  5077  triun  5210  ralxfrd  5344  ralxfrd2  5348  elrnmptg  5900  fmpt  7043  fliftfun  7246  fiunlem  7874  fiun  7875  f1iun  7876  omabs  8566  findcard3  9167  r1sdom  9667  tcrank  9777  infxpenlem  9904  dfac12k  10039  cfslb2n  10159  cfcoflem  10163  iundom2g  10431  supsrlem  11002  axpre-sup  11060  fimaxre3  12068  hashgt23el  14331  limsupbnd2  15390  rlimuni  15457  rlimcld2  15485  rlimno1  15561  pgpfac1lem5  19993  rhmdvdsr  20423  ppttop  22922  epttop  22924  tgcnp  23168  lmcnp  23219  bwth  23325  1stcrest  23368  txlm  23563  tx1stc  23565  fbfinnfr  23756  fbunfip  23784  filuni  23800  ufileu  23834  fbflim2  23892  flftg  23911  ufilcmp  23947  cnpfcf  23956  tsmsxp  24070  metss  24423  lmmbr  25185  ivthlem2  25380  ivthlem3  25381  dyadmax  25526  tpr2rico  33925  esumpcvgval  34091  sigaclcuni  34131  voliune  34242  volfiniune  34243  dya2icoseg2  34291  onvf1odlem1  35147  umgr2cycllem  35184  umgr2cycl  35185  poimirlem29  37697  unirep  37762  heibor1lem  37857  pmapglbx  39816  stoweidlem35  46081