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  7939  fiun  7940  f1iun  7941  omabs  8637  findcard3  9243  r1sdom  9746  tcrank  9856  infxpenlem  9997  dfac12k  10131  cfslb2n  10252  cfcoflem  10256  iundom2g  10524  supsrlem  11096  axpre-sup  11154  fimaxre3  12161  hashgt23el  14461  limsupbnd2  15534  rlimuni  15601  rlimcld2  15629  rlimno1  15705  pgpfac1lem5  20151  rhmdvdsr  20591  ppttop  23133  epttop  23135  tgcnp  23379  lmcnp  23430  bwth  23536  1stcrest  23579  txlm  23774  tx1stc  23776  fbfinnfr  23967  fbunfip  23995  filuni  24011  ufileu  24045  fbflim2  24103  flftg  24122  ufilcmp  24158  cnpfcf  24167  tsmsxp  24281  metss  24634  lmmbr  25386  ivthlem2  25580  ivthlem3  25581  dyadmax  25726  tpr2rico  34247  esumpcvgval  34413  sigaclcuni  34453  voliune  34564  volfiniune  34565  dya2icoseg2  34613  onvf1odlem1  35520  umgr2cycllem  35565  umgr2cycl  35566  poimirlem29  38222  unirep  38287  heibor1lem  38382  pmapglbx  40467  stoweidlem35  46675