Theorem r19.29 3102

Description: Restricted quantifier version of 19.29 1880. See also r19.29r 3103. (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 533	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3096	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpa 477	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 396  ∀wral 3053  ∃wrex 3063

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3054  df-rex 3064

This theorem is referenced by:  2r19.29  3125  disjiun  5060  triun  5194  ralxfrd  5337  ralxfrd2  5341  elrnmptg  5903  fmpt  7051  fliftfun  7256  fiunlem  7884  fiun  7885  f1iun  7886  omabs  8577  findcard3  9183  r1sdom  9689  tcrank  9799  infxpenlem  9926  dfac12k  10061  cfslb2n  10181  cfcoflem  10185  iundom2g  10453  supsrlem  11025  axpre-sup  11083  fimaxre3  12093  hashgt23el  14377  limsupbnd2  15436  rlimuni  15503  rlimcld2  15531  rlimno1  15607  pgpfac1lem5  20047  rhmdvdsr  20480  ppttop  22990  epttop  22992  tgcnp  23236  lmcnp  23287  bwth  23393  1stcrest  23436  txlm  23631  tx1stc  23633  fbfinnfr  23824  fbunfip  23852  filuni  23868  ufileu  23902  fbflim2  23960  flftg  23979  ufilcmp  24015  cnpfcf  24024  tsmsxp  24138  metss  24491  lmmbr  25243  ivthlem2  25437  ivthlem3  25438  dyadmax  25583  tpr2rico  34096  esumpcvgval  34262  sigaclcuni  34302  voliune  34413  volfiniune  34414  dya2icoseg2  34462  onvf1odlem1  35331  umgr2cycllem  35368  umgr2cycl  35369  poimirlem29  38016  unirep  38081  heibor1lem  38176  pmapglbx  40261  stoweidlem35  46478