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 3252
Description: Restricted quantifier version of 19.29r 1974; variation of r19.29 3251. (Contributed by NM, 31-Aug-1999.)
Assertion
Ref Expression
r19.29r ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))

Proof of Theorem r19.29r
StepHypRef Expression
1 r19.29 3251 . 2 ((∀𝑥𝐴 𝜓 ∧ ∃𝑥𝐴 𝜑) → ∃𝑥𝐴 (𝜓𝜑))
2 ancom 453 . 2 ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) ↔ (∀𝑥𝐴 𝜓 ∧ ∃𝑥𝐴 𝜑))
3 ancom 453 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
43rexbii 3220 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴 (𝜓𝜑))
51, 2, 43imtr4i 284 1 ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  wral 3087  wrex 3088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-ral 3092  df-rex 3093
This theorem is referenced by:  r19.29imd  3253  2reu5  3612  rlimuni  14618  rlimno1  14721  neindisj2  21252  lmss  21427  fclsbas  22149  isfcf  22162  ucnima  22409  metcnp3  22669  cfilucfil  22688  bndth  23081  ellimc3  23980  lmxrge0  30505  gsumesum  30628  esumcst  30632  esumfsup  30639  voliune  30799  volfiniune  30800  bnj517  31463  cover2  33987  prmunb2  39279
  Copyright terms: Public domain W3C validator