Theorem r19.29 3102

Description: Restricted quantifier version of 19.29 1873. See also r19.29r 3104. (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 3061

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

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

This theorem is referenced by:  r19.29rOLD  3105  2r19.29  3127  disjiun  5112  triun  5249  ralxfrd  5383  ralxfrd2  5387  elrnmptg  5946  fmpt  7105  fliftfun  7310  fiunlem  7945  fiun  7946  f1iun  7947  omabs  8668  findcard3  9295  findcard3OLD  9296  r1sdom  9793  tcrank  9903  infxpenlem  10032  dfac12k  10167  cfslb2n  10287  cfcoflem  10291  iundom2g  10559  supsrlem  11130  axpre-sup  11188  fimaxre3  12193  hashgt23el  14447  limsupbnd2  15504  rlimuni  15571  rlimcld2  15599  rlimno1  15675  pgpfac1lem5  20067  rhmdvdsr  20473  ppttop  22950  epttop  22952  tgcnp  23196  lmcnp  23247  bwth  23353  1stcrest  23396  txlm  23591  tx1stc  23593  fbfinnfr  23784  fbunfip  23812  filuni  23828  ufileu  23862  fbflim2  23920  flftg  23939  ufilcmp  23975  cnpfcf  23984  tsmsxp  24098  metss  24452  lmmbr  25215  ivthlem2  25410  ivthlem3  25411  dyadmax  25556  tpr2rico  33948  esumpcvgval  34114  sigaclcuni  34154  voliune  34265  volfiniune  34266  dya2icoseg2  34315  umgr2cycllem  35167  umgr2cycl  35168  poimirlem29  37678  unirep  37743  heibor1lem  37838  pmapglbx  39793  stoweidlem35  46044