Theorem r19.29 3134

Description: Restricted quantifier version of 19.29 1900. See also r19.29r 3135. (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 537	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3128	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpa 481	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 400  ∀wral 3085  ∃wrex 3095

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-ral 3086  df-rex 3096

This theorem is referenced by:  2r19.29  3157  disjiun  5101  triun  5237  ralxfrd  5380  ralxfrd2  5384  elrnmptg  5952  fmpt  7106  fliftfun  7311  fiunlem  7938  fiun  7939  f1iun  7940  omabs  8636  findcard3  9242  r1sdom  9745  tcrank  9855  infxpenlem  9996  dfac12k  10130  cfslb2n  10251  cfcoflem  10255  iundom2g  10523  supsrlem  11095  axpre-sup  11153  fimaxre3  12160  hashgt23el  14460  limsupbnd2  15533  rlimuni  15600  rlimcld2  15628  rlimno1  15704  pgpfac1lem5  20150  rhmdvdsr  20590  ppttop  23132  epttop  23134  tgcnp  23378  lmcnp  23429  bwth  23535  1stcrest  23578  txlm  23773  tx1stc  23775  fbfinnfr  23966  fbunfip  23994  filuni  24010  ufileu  24044  fbflim2  24102  flftg  24121  ufilcmp  24157  cnpfcf  24166  tsmsxp  24280  metss  24633  lmmbr  25385  ivthlem2  25579  ivthlem3  25580  dyadmax  25725  tpr2rico  34246  esumpcvgval  34412  sigaclcuni  34452  voliune  34563  volfiniune  34564  dya2icoseg2  34612  onvf1odlem1  35485  umgr2cycllem  35530  umgr2cycl  35531  poimirlem29  38187  unirep  38252  heibor1lem  38347  pmapglbx  40432  stoweidlem35  46640