Theorem r19.29 3113

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3060  ∃wrex 3069

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-ral 3061  df-rex 3070

This theorem is referenced by:  r19.29rOLD  3116  2r19.29  3138  r19.29d2rOLD  3140  disjiun  5130  triun  5273  ralxfrd  5407  ralxfrd2  5411  elrnmptg  5971  fmpt  7129  fliftfun  7333  fiunlem  7967  fiun  7968  f1iun  7969  omabs  8690  findcard3  9319  findcard3OLD  9320  r1sdom  9815  tcrank  9925  infxpenlem  10054  dfac12k  10189  cfslb2n  10309  cfcoflem  10313  iundom2g  10581  supsrlem  11152  axpre-sup  11210  fimaxre3  12215  hashgt23el  14464  limsupbnd2  15520  rlimuni  15587  rlimcld2  15615  rlimno1  15691  pgpfac1lem5  20100  rhmdvdsr  20509  ppttop  23015  epttop  23017  tgcnp  23262  lmcnp  23313  bwth  23419  1stcrest  23462  txlm  23657  tx1stc  23659  fbfinnfr  23850  fbunfip  23878  filuni  23894  ufileu  23928  fbflim2  23986  flftg  24005  ufilcmp  24041  cnpfcf  24050  tsmsxp  24164  metss  24522  lmmbr  25293  ivthlem2  25488  ivthlem3  25489  dyadmax  25634  tpr2rico  33912  esumpcvgval  34080  sigaclcuni  34120  voliune  34231  volfiniune  34232  dya2icoseg2  34281  umgr2cycllem  35146  umgr2cycl  35147  poimirlem29  37657  unirep  37722  heibor1lem  37817  pmapglbx  39772  stoweidlem35  46055