Theorem r19.29 3125

Description: Restricted quantifier version of 19.29 1893. 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 536	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3119	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpa 480	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 399  ∀wral 3076  ∃wrex 3086

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-ral 3077  df-rex 3087

This theorem is referenced by:  2r19.29  3148  disjiun  5088  triun  5222  ralxfrd  5365  ralxfrd2  5369  elrnmptg  5937  fmpt  7091  fliftfun  7296  fiunlem  7923  fiun  7924  f1iun  7925  omabs  8621  findcard3  9227  r1sdom  9732  tcrank  9842  infxpenlem  9969  dfac12k  10104  cfslb2n  10225  cfcoflem  10229  iundom2g  10497  supsrlem  11069  axpre-sup  11127  fimaxre3  12138  hashgt23el  14437  limsupbnd2  15510  rlimuni  15577  rlimcld2  15605  rlimno1  15681  pgpfac1lem5  20121  rhmdvdsr  20554  ppttop  23064  epttop  23066  tgcnp  23310  lmcnp  23361  bwth  23467  1stcrest  23510  txlm  23705  tx1stc  23707  fbfinnfr  23898  fbunfip  23926  filuni  23942  ufileu  23976  fbflim2  24034  flftg  24053  ufilcmp  24089  cnpfcf  24098  tsmsxp  24212  metss  24565  lmmbr  25317  ivthlem2  25511  ivthlem3  25512  dyadmax  25657  tpr2rico  34206  esumpcvgval  34372  sigaclcuni  34412  voliune  34523  volfiniune  34524  dya2icoseg2  34572  onvf1odlem1  35443  umgr2cycllem  35487  umgr2cycl  35488  poimirlem29  38145  unirep  38210  heibor1lem  38305  pmapglbx  40390  stoweidlem35  46606