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

Theorem r19.2z 4012
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1879). The restricted version is valid only when the domain of quantification is not empty. (Contributed by NM, 15-Nov-2003.)
Assertion
Ref Expression
r19.2z ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝜑) → ∃𝑥𝐴 𝜑)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem r19.2z
StepHypRef Expression
1 df-ral 2901 . . . 4 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 exintr 1810 . . . 4 (∀𝑥(𝑥𝐴𝜑) → (∃𝑥 𝑥𝐴 → ∃𝑥(𝑥𝐴𝜑)))
31, 2sylbi 206 . . 3 (∀𝑥𝐴 𝜑 → (∃𝑥 𝑥𝐴 → ∃𝑥(𝑥𝐴𝜑)))
4 n0 3890 . . 3 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
5 df-rex 2902 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
63, 4, 53imtr4g 284 . 2 (∀𝑥𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥𝐴 𝜑))
76impcom 445 1 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝜑) → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wal 1473  wex 1695  wcel 1977  wne 2780  wral 2896  wrex 2897  c0 3874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-v 3175  df-dif 3543  df-nul 3875
This theorem is referenced by:  r19.2zb  4013  intssuni  4429  riinn0  4526  trintss  4692  iinexg  4746  reusv2lem2  4790  reusv2lem2OLD  4791  reusv2lem3  4792  xpiindi  5167  cnviin  5575  eusvobj2  6520  iiner  7684  finsschain  8134  cfeq0  8939  cfsuc  8940  iundom2g  9219  alephval2  9251  prlem934  9712  supaddc  10840  supadd  10841  supmul1  10842  supmullem2  10844  supmul  10845  rexfiuz  13884  r19.2uz  13888  climuni  14080  caurcvg  14204  caurcvg2  14205  caucvg  14206  pc2dvds  15370  vdwmc2  15470  vdwlem6  15477  vdwnnlem3  15488  issubg4  17385  gexcl3  17774  lbsextlem2  18929  iincld  20601  opnnei  20682  cncnp2  20843  lmmo  20942  iuncon  20989  ptbasfi  21142  filuni  21447  isfcls  21571  fclsopn  21576  ustfilxp  21774  nrginvrcn  22254  lebnumlem3  22518  cfil3i  22820  caun0  22832  iscmet3  22844  nulmbl2  23056  dyadmax  23117  itg2seq  23260  itg2monolem1  23268  rolle  23502  c1lip1  23509  taylfval  23862  ulm0  23894  usgreghash2spot  26390  bnj906  30048  cvmliftlem15  30328  dfon2lem6  30731  filnetlem4  31340  itg2addnclem  32425  itg2addnc  32428  itg2gt0cn  32429  bddiblnc  32444  ftc1anc  32457  filbcmb  32499  incsequz  32508  isbnd2  32546  isbnd3  32547  ssbnd  32551  unichnidl  32794  iunconlem2  37987  upbdrech  38254  fusgreghash2wsp  41494  av-frgrareg  41540
  Copyright terms: Public domain W3C validator