Theorem r19.29 3100

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3051  ∃wrex 3061

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3052  df-rex 3062

This theorem is referenced by:  2r19.29  3123  disjiun  5073  triun  5207  ralxfrd  5350  ralxfrd2  5354  elrnmptg  5916  fmpt  7062  fliftfun  7267  fiunlem  7895  fiun  7896  f1iun  7897  omabs  8587  findcard3  9193  r1sdom  9698  tcrank  9808  infxpenlem  9935  dfac12k  10070  cfslb2n  10190  cfcoflem  10194  iundom2g  10462  supsrlem  11034  axpre-sup  11092  fimaxre3  12102  hashgt23el  14386  limsupbnd2  15445  rlimuni  15512  rlimcld2  15540  rlimno1  15616  pgpfac1lem5  20056  rhmdvdsr  20485  ppttop  22972  epttop  22974  tgcnp  23218  lmcnp  23269  bwth  23375  1stcrest  23418  txlm  23613  tx1stc  23615  fbfinnfr  23806  fbunfip  23834  filuni  23850  ufileu  23884  fbflim2  23942  flftg  23961  ufilcmp  23997  cnpfcf  24006  tsmsxp  24120  metss  24473  lmmbr  25225  ivthlem2  25419  ivthlem3  25420  dyadmax  25565  tpr2rico  34056  esumpcvgval  34222  sigaclcuni  34262  voliune  34373  volfiniune  34374  dya2icoseg2  34422  onvf1odlem1  35285  umgr2cycllem  35322  umgr2cycl  35323  poimirlem29  37970  unirep  38035  heibor1lem  38130  pmapglbx  40215  stoweidlem35  46463