Theorem r19.29 3112

Description: Restricted quantifier version of 19.29 1871. See also r19.29r 3114. (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 3104	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpa 476	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3059  ∃wrex 3068

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-ral 3060  df-rex 3069

This theorem is referenced by:  r19.29rOLD  3115  2r19.29  3137  r19.29d2rOLD  3139  disjiun  5136  triun  5280  ralxfrd  5414  ralxfrd2  5418  elrnmptg  5975  fmpt  7130  fliftfun  7332  fiunlem  7965  fiun  7966  f1iun  7967  omabs  8688  findcard3  9316  findcard3OLD  9317  r1sdom  9812  tcrank  9922  infxpenlem  10051  dfac12k  10186  cfslb2n  10306  cfcoflem  10310  iundom2g  10578  supsrlem  11149  axpre-sup  11207  fimaxre3  12212  hashgt23el  14460  limsupbnd2  15516  rlimuni  15583  rlimcld2  15611  rlimno1  15687  pgpfac1lem5  20114  rhmdvdsr  20525  ppttop  23030  epttop  23032  tgcnp  23277  lmcnp  23328  bwth  23434  1stcrest  23477  txlm  23672  tx1stc  23674  fbfinnfr  23865  fbunfip  23893  filuni  23909  ufileu  23943  fbflim2  24001  flftg  24020  ufilcmp  24056  cnpfcf  24065  tsmsxp  24179  metss  24537  lmmbr  25306  ivthlem2  25501  ivthlem3  25502  dyadmax  25647  tpr2rico  33873  esumpcvgval  34059  sigaclcuni  34099  voliune  34210  volfiniune  34211  dya2icoseg2  34260  umgr2cycllem  35125  umgr2cycl  35126  poimirlem29  37636  unirep  37701  heibor1lem  37796  pmapglbx  39752  stoweidlem35  45991