Theorem r19.29 3101

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3052  ∃wrex 3062

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 3053  df-rex 3063

This theorem is referenced by:  2r19.29  3124  disjiun  5074  triun  5208  ralxfrd  5346  ralxfrd2  5350  elrnmptg  5911  fmpt  7057  fliftfun  7261  fiunlem  7889  fiun  7890  f1iun  7891  omabs  8581  findcard3  9187  r1sdom  9692  tcrank  9802  infxpenlem  9929  dfac12k  10064  cfslb2n  10184  cfcoflem  10188  iundom2g  10456  supsrlem  11028  axpre-sup  11086  fimaxre3  12096  hashgt23el  14380  limsupbnd2  15439  rlimuni  15506  rlimcld2  15534  rlimno1  15610  pgpfac1lem5  20050  rhmdvdsr  20479  ppttop  22985  epttop  22987  tgcnp  23231  lmcnp  23282  bwth  23388  1stcrest  23431  txlm  23626  tx1stc  23628  fbfinnfr  23819  fbunfip  23847  filuni  23863  ufileu  23897  fbflim2  23955  flftg  23974  ufilcmp  24010  cnpfcf  24019  tsmsxp  24133  metss  24486  lmmbr  25238  ivthlem2  25432  ivthlem3  25433  dyadmax  25578  tpr2rico  34075  esumpcvgval  34241  sigaclcuni  34281  voliune  34392  volfiniune  34393  dya2icoseg2  34441  onvf1odlem1  35304  umgr2cycllem  35341  umgr2cycl  35342  poimirlem29  37987  unirep  38052  heibor1lem  38147  pmapglbx  40232  stoweidlem35  46484