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

Theorem r19.2z 3653
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1666). 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 2647 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1621 . . . 4  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
31, 2sylbi 188 . . 3  |-  ( A. x  e.  A  ph  ->  ( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
4 n0 3573 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2648 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
63, 4, 53imtr4g 262 . 2  |-  ( A. x  e.  A  ph  ->  ( A  =/=  (/)  ->  E. x  e.  A  ph ) )
76impcom 420 1  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1546   E.wex 1547    e. wcel 1717    =/= wne 2543   A.wral 2642   E.wrex 2643   (/)c0 3564
This theorem is referenced by:  r19.2zb  3654  intssuni  4007  riinn0  4099  trintss  4252  iinexg  4294  reusv2lem2  4658  reusv2lem3  4659  reusv6OLD  4667  xpiindi  4943  cnviin  5342  eusvobj2  6511  iiner  6905  finsschain  7341  cfeq0  8062  cfsuc  8063  iundom2g  8341  alephval2  8373  prlem934  8836  supmul1  9898  supmullem2  9900  supmul  9901  rexfiuz  12071  r19.2uz  12075  climuni  12266  caurcvg  12390  caurcvg2  12391  caucvg  12392  pc2dvds  13172  vdwmc2  13267  vdwlem6  13274  vdwnnlem3  13285  issubg4  14881  gexcl3  15141  lbsextlem2  16151  iincld  17019  opnnei  17100  cncnp2  17260  lmmo  17359  iuncon  17405  ptbasfi  17527  filuni  17831  isfcls  17955  fclsopn  17960  ustfilxp  18156  nrginvrcn  18591  lebnumlem3  18852  cfil3i  19086  caun0  19098  iscmet3  19110  nulmbl2  19291  dyadmax  19350  itg2seq  19494  itg2monolem1  19502  rolle  19734  c1lip1  19741  taylfval  20135  ulm0  20167  isgrp2d  21664  cvmliftlem15  24757  dfon2lem6  25161  supaddc  25940  supadd  25941  itg2gt0cn  25953  bddiblnc  25968  filnetlem4  26094  filbcmb  26126  incsequz  26136  isbnd2  26176  isbnd3  26177  ssbnd  26181  unichnidl  26325  bnj906  28632
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-ral 2647  df-rex 2648  df-v 2894  df-dif 3259  df-nul 3565
  Copyright terms: Public domain W3C validator