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

Theorem r19.2z 3545
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1673). 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 2550 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1603 . . . 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 3466 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2551 . . 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 1529   E.wex 1530    e. wcel 1686    =/= wne 2448   A.wral 2545   E.wrex 2546   (/)c0 3457
This theorem is referenced by:  r19.2zb  3546  intssuni  3886  riinn0  3978  trintss  4131  iinexg  4173  reusv2lem2  4538  reusv2lem3  4539  reusv6OLD  4547  xpiindi  4823  cnviin  5214  eusvobj2  6339  iiner  6733  finsschain  7164  cfeq0  7884  cfsuc  7885  iundom2g  8164  alephval2  8196  prlem934  8659  supmul1  9721  supmullem2  9723  supmul  9724  rexfiuz  11833  r19.2uz  11837  climuni  12028  caurcvg  12151  caurcvg2  12152  caucvg  12153  pc2dvds  12933  vdwmc2  13028  vdwlem6  13035  vdwnnlem3  13046  issubg4  14640  gexcl3  14900  lbsextlem2  15914  iincld  16778  opnnei  16859  cncnp2  17012  lmmo  17110  iuncon  17156  ptbasfi  17278  filuni  17582  isfcls  17706  fclsopn  17711  nrginvrcn  18204  lebnumlem3  18463  cfil3i  18697  caun0  18709  iscmet3  18721  nulmbl2  18896  dyadmax  18955  itg2seq  19099  itg2monolem1  19107  rolle  19339  c1lip1  19346  taylfval  19740  ulm0  19772  isgrp2d  20904  cvmliftlem15  23831  dfon2lem6  24146  supaddc  24927  supadd  24928  r19.2zr  24968  rexlimib  24970  lvsovso3  25639  filnetlem4  26341  filbcmb  26443  incsequz  26469  isbnd2  26518  isbnd3  26519  ssbnd  26523  unichnidl  26667  bnj906  29035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-v 2792  df-dif 3157  df-nul 3458
  Copyright terms: Public domain W3C validator