Theorem r19.29 3126

Description: Restricted quantifier version of 19.29 1906. See also r19.29r 3127. (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 538	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3120	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpa 482	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wral 3077  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3078  df-rex 3088

This theorem is used by:  2r19.29  3149  disjiun  5091  triun  5227  ralxfrd  5370  ralxfrd2  5374  elrnmptg  5943  fmpt  7108  fliftfun  7318  fiunlem  7952  fiun  7953  f1iun  7954  omabs  8653  findcard3  9267  r1sdom  9774  tcrank  9894  infxpenlem  10085  dfac12k  10219  cfslb2n  10339  cfcoflem  10343  iundom2g  10617  supsrlem  11189  axpre-sup  11247  fimaxre3  12256  hashgt23el  14562  limsupbnd2  15643  rlimuni  15710  rlimcld2  15738  rlimno1  15814  pgpfac1lem5  20288  rhmdvdsr  20751  ppttop  23318  epttop  23320  tgcnp  23564  lmcnp  23615  bwth  23721  1stcrest  23764  txlm  23960  tx1stc  23962  fbfinnfr  24153  fbunfip  24181  filuni  24197  ufileu  24231  fbflim2  24289  flftg  24308  ufilcmp  24344  cnpfcf  24353  tsmsxp  24467  metss  24820  lmmbr  25572  ivthlem2  25766  ivthlem3  25767  dyadmax  25912  umgr2cycllem  30739  umgr2cycl  30740  tpr2rico  34537  esumpcvgval  34703  sigaclcuni  34743  voliune  34855  volfiniune  34856  dya2icoseg2  34903  onvf1odlem1  35865  poimirlem29  38547  unirep  38628  heibor1lem  38723  pmapglbx  40806  stoweidlem35  47014