MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.29r Structured version   Visualization version   GIF version

Theorem r19.29r 3116
Description: Restricted quantifier version of 19.29r 1874; variation of r19.29 3114. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Wolf Lammen, 29-Jun-2023.)
Assertion
Ref Expression
r19.29r ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))

Proof of Theorem r19.29r
StepHypRef Expression
1 iba 527 . . 3 (𝜓 → (𝜑 ↔ (𝜑𝜓)))
21ralrexbid 3106 . 2 (∀𝑥𝐴 𝜓 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 (𝜑𝜓)))
32biimpac 478 1 ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wral 3061  wrex 3070
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 3062  df-rex 3071
This theorem is referenced by:  r19.29imd  3118  2reu5  3764  rlimuni  15586  rlimno1  15690  neindisj2  23131  lmss  23306  fclsbas  24029  isfcf  24042  ucnima  24290  metcnp3  24553  cfilucfil  24572  bndth  24990  ellimc3  25914  lmxrge0  33951  gsumesum  34060  esumcst  34064  esumfsup  34071  voliune  34230  volfiniune  34231  bnj517  34899  nummin  35105  fvineqsneq  37413  cover2  37722  naddgeoa  43407  prmunb2  44330
  Copyright terms: Public domain W3C validator