Theorem r19.29 3094

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3044  ∃wrex 3053

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 3045  df-rex 3054

This theorem is referenced by:  r19.29rOLD  3097  2r19.29  3119  disjiun  5095  triun  5229  ralxfrd  5363  ralxfrd2  5367  elrnmptg  5925  fmpt  7082  fliftfun  7287  fiunlem  7920  fiun  7921  f1iun  7922  omabs  8615  findcard3  9229  findcard3OLD  9230  r1sdom  9727  tcrank  9837  infxpenlem  9966  dfac12k  10101  cfslb2n  10221  cfcoflem  10225  iundom2g  10493  supsrlem  11064  axpre-sup  11122  fimaxre3  12129  hashgt23el  14389  limsupbnd2  15449  rlimuni  15516  rlimcld2  15544  rlimno1  15620  pgpfac1lem5  20011  rhmdvdsr  20417  ppttop  22894  epttop  22896  tgcnp  23140  lmcnp  23191  bwth  23297  1stcrest  23340  txlm  23535  tx1stc  23537  fbfinnfr  23728  fbunfip  23756  filuni  23772  ufileu  23806  fbflim2  23864  flftg  23883  ufilcmp  23919  cnpfcf  23928  tsmsxp  24042  metss  24396  lmmbr  25158  ivthlem2  25353  ivthlem3  25354  dyadmax  25499  tpr2rico  33902  esumpcvgval  34068  sigaclcuni  34108  voliune  34219  volfiniune  34220  dya2icoseg2  34269  onvf1odlem1  35090  umgr2cycllem  35127  umgr2cycl  35128  poimirlem29  37643  unirep  37708  heibor1lem  37803  pmapglbx  39763  stoweidlem35  46033