Theorem r19.29 3125

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

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

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-ral 3077  df-rex 3087

This theorem is used by:  2r19.29  3148  disjiun  5090  triun  5226  ralxfrd  5370  ralxfrd2  5374  elrnmptg  5944  fmpt  7115  fliftfun  7324  fiunlem  7958  fiun  7959  f1iun  7960  omabs  8667  findcard3  9281  r1sdom  9788  tcrank  9908  infxpenlem  10099  dfac12k  10233  cfslb2n  10353  cfcoflem  10357  iundom2g  10631  supsrlem  11203  axpre-sup  11261  fimaxre3  12270  hashgt23el  14576  limsupbnd2  15659  rlimuni  15726  rlimcld2  15754  rlimno1  15830  pgpfac1lem5  20304  rhmdvdsr  20767  ppttop  23334  epttop  23336  tgcnp  23580  lmcnp  23631  bwth  23737  1stcrest  23780  txlm  23976  tx1stc  23978  fbfinnfr  24169  fbunfip  24197  filuni  24213  ufileu  24247  fbflim2  24305  flftg  24324  ufilcmp  24360  cnpfcf  24369  tsmsxp  24483  metss  24836  lmmbr  25588  ivthlem2  25782  ivthlem3  25783  dyadmax  25928  umgr2cycllem  30755  umgr2cycl  30756  tpr2rico  34594  esumpcvgval  34760  sigaclcuni  34800  voliune  34912  volfiniune  34913  dya2icoseg2  34960  onvf1odlem1  35954  poimirlem29  38676  unirep  38757  heibor1lem  38852  pmapglbx  40935  stoweidlem35  47153