Theorem r19.29 3101

Description: Restricted quantifier version of 19.29 1875. See also r19.29r 3102. (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 528	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3095	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpa 476	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3052  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053  df-rex 3063

This theorem is referenced by:  2r19.29  3124  disjiun  5088  triun  5221  ralxfrd  5355  ralxfrd2  5359  elrnmptg  5918  fmpt  7064  fliftfun  7268  fiunlem  7896  fiun  7897  f1iun  7898  omabs  8589  findcard3  9195  r1sdom  9698  tcrank  9808  infxpenlem  9935  dfac12k  10070  cfslb2n  10190  cfcoflem  10194  iundom2g  10462  supsrlem  11034  axpre-sup  11092  fimaxre3  12100  hashgt23el  14359  limsupbnd2  15418  rlimuni  15485  rlimcld2  15513  rlimno1  15589  pgpfac1lem5  20022  rhmdvdsr  20453  ppttop  22963  epttop  22965  tgcnp  23209  lmcnp  23260  bwth  23366  1stcrest  23409  txlm  23604  tx1stc  23606  fbfinnfr  23797  fbunfip  23825  filuni  23841  ufileu  23875  fbflim2  23933  flftg  23952  ufilcmp  23988  cnpfcf  23997  tsmsxp  24111  metss  24464  lmmbr  25226  ivthlem2  25421  ivthlem3  25422  dyadmax  25567  tpr2rico  34090  esumpcvgval  34256  sigaclcuni  34296  voliune  34407  volfiniune  34408  dya2icoseg2  34456  onvf1odlem1  35319  umgr2cycllem  35356  umgr2cycl  35357  poimirlem29  37900  unirep  37965  heibor1lem  38060  pmapglbx  40145  stoweidlem35  46393