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

Theorem r19.2z 3577
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1650). 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 2582 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1605 . . . 4  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
31, 2sylbi 187 . . 3  |-  ( A. x  e.  A  ph  ->  ( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
4 n0 3498 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2583 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
63, 4, 53imtr4g 261 . 2  |-  ( A. x  e.  A  ph  ->  ( A  =/=  (/)  ->  E. x  e.  A  ph ) )
76impcom 419 1  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1531   E.wex 1532    e. wcel 1701    =/= wne 2479   A.wral 2577   E.wrex 2578   (/)c0 3489
This theorem is referenced by:  r19.2zb  3578  intssuni  3921  riinn0  4013  trintss  4166  iinexg  4208  reusv2lem2  4573  reusv2lem3  4574  reusv6OLD  4582  xpiindi  4858  cnviin  5249  eusvobj2  6379  iiner  6773  finsschain  7207  cfeq0  7927  cfsuc  7928  iundom2g  8207  alephval2  8239  prlem934  8702  supmul1  9764  supmullem2  9766  supmul  9767  rexfiuz  11878  r19.2uz  11882  climuni  12073  caurcvg  12196  caurcvg2  12197  caucvg  12198  pc2dvds  12978  vdwmc2  13073  vdwlem6  13080  vdwnnlem3  13091  issubg4  14687  gexcl3  14947  lbsextlem2  15961  iincld  16832  opnnei  16913  cncnp2  17066  lmmo  17164  iuncon  17210  ptbasfi  17332  filuni  17632  isfcls  17756  fclsopn  17761  nrginvrcn  18254  lebnumlem3  18514  cfil3i  18748  caun0  18760  iscmet3  18772  nulmbl2  18947  dyadmax  19006  itg2seq  19150  itg2monolem1  19158  rolle  19390  c1lip1  19397  taylfval  19791  ulm0  19823  isgrp2d  20955  ustfilxp  23429  cvmliftlem15  24113  dfon2lem6  24529  supaddc  25309  supadd  25310  itg2gt0cn  25320  bddiblnc  25335  filnetlem4  25479  filbcmb  25581  incsequz  25607  isbnd2  25655  isbnd3  25656  ssbnd  25660  unichnidl  25804  bnj906  28473
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-v 2824  df-dif 3189  df-nul 3490
  Copyright terms: Public domain W3C validator