Theorem r19.29 3125

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

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

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 3077  df-rex 3087

This theorem is used by:  2r19.29  3148  disjiun  5091  triun  5227  ralxfrd  5373  ralxfrd2  5377  elrnmptg  5945  fmpt  7103  fliftfun  7313  fiunlem  7939  fiun  7940  f1iun  7941  omabs  8639  findcard3  9253  r1sdom  9756  tcrank  9866  infxpenlem  10016  dfac12k  10150  cfslb2n  10270  cfcoflem  10274  iundom2g  10548  supsrlem  11120  axpre-sup  11178  fimaxre3  12185  hashgt23el  14489  limsupbnd2  15570  rlimuni  15637  rlimcld2  15665  rlimno1  15741  pgpfac1lem5  20208  rhmdvdsr  20668  ppttop  23232  epttop  23234  tgcnp  23478  lmcnp  23529  bwth  23635  1stcrest  23678  txlm  23874  tx1stc  23876  fbfinnfr  24067  fbunfip  24095  filuni  24111  ufileu  24145  fbflim2  24203  flftg  24222  ufilcmp  24258  cnpfcf  24267  tsmsxp  24381  metss  24734  lmmbr  25486  ivthlem2  25680  ivthlem3  25681  dyadmax  25826  umgr2cycllem  30625  umgr2cycl  30626  tpr2rico  34422  esumpcvgval  34588  sigaclcuni  34628  voliune  34740  volfiniune  34741  dya2icoseg2  34789  onvf1odlem1  35700  poimirlem29  38398  unirep  38464  heibor1lem  38559  pmapglbx  40642  stoweidlem35  46863