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

Theorem r19.2z 3888
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1802). 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  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  ph )  ->  E. x  e.  A  ph )
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem r19.2z
StepHypRef Expression
1 df-ral 2776 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1750 . . . 4  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
31, 2sylbi 198 . . 3  |-  ( A. x  e.  A  ph  ->  ( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
4 n0 3771 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2777 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
63, 4, 53imtr4g 273 . 2  |-  ( A. x  e.  A  ph  ->  ( A  =/=  (/)  ->  E. x  e.  A  ph ) )
76impcom 431 1  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   A.wal 1435   E.wex 1657    e. wcel 1872    =/= wne 2614   A.wral 2771   E.wrex 2772   (/)c0 3761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-v 3082  df-dif 3439  df-nul 3762
This theorem is referenced by:  r19.2zb  3889  intssuni  4278  riinn0  4374  trintss  4534  iinexg  4584  reusv2lem2  4626  reusv2lem3  4627  xpiindi  4989  cnviin  5392  eusvobj2  6298  iiner  7446  finsschain  7890  cfeq0  8693  cfsuc  8694  iundom2g  8972  alephval2  9004  prlem934  9465  supaddc  10581  supadd  10582  supmul1  10583  supmullem2  10585  supmul  10586  rexfiuz  13410  r19.2uz  13414  climuni  13615  caurcvg  13741  caurcvgOLD  13742  caurcvg2  13743  caucvg  13744  pc2dvds  14827  vdwmc2  14928  vdwlem6  14935  vdwnnlem3  14946  issubg4  16835  gexcl3  17238  lbsextlem2  18381  iincld  20052  opnnei  20134  cncnp2  20295  lmmo  20394  iuncon  20441  ptbasfi  20594  filuni  20898  isfcls  21022  fclsopn  21027  ustfilxp  21225  nrginvrcn  21692  lebnumlem3  21989  lebnumlem3OLD  21992  cfil3i  22237  caun0  22249  iscmet3  22261  nulmbl2  22488  dyadmax  22554  itg2seq  22698  itg2monolem1  22706  rolle  22940  c1lip1  22947  taylfval  23312  ulm0  23344  usgreghash2spot  25795  isgrp2d  25961  bnj906  29749  cvmliftlem15  30029  dfon2lem6  30441  filnetlem4  31042  itg2addnclem  31957  itg2addnc  31960  itg2gt0cn  31961  bddiblnc  31976  ftc1anc  31989  filbcmb  32031  incsequz  32041  isbnd2  32079  isbnd3  32080  ssbnd  32084  unichnidl  32228  iunconlem2  37305  upbdrech  37477
  Copyright terms: Public domain W3C validator