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

Theorem r19.2z 3543
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1671). 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 2548 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1601 . . . 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 3464 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2549 . . 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 1527   E.wex 1528    e. wcel 1684    =/= wne 2446   A.wral 2543   E.wrex 2544   (/)c0 3455
This theorem is referenced by:  r19.2zb  3544  intssuni  3884  riinn0  3976  trintss  4129  iinexg  4171  reusv2lem2  4536  reusv2lem3  4537  reusv6OLD  4545  xpiindi  4821  cnviin  5212  eusvobj2  6337  iiner  6731  finsschain  7162  cfeq0  7882  cfsuc  7883  iundom2g  8162  alephval2  8194  prlem934  8657  supmul1  9719  supmullem2  9721  supmul  9722  rexfiuz  11831  r19.2uz  11835  climuni  12026  caurcvg  12149  caurcvg2  12150  caucvg  12151  pc2dvds  12931  vdwmc2  13026  vdwlem6  13033  vdwnnlem3  13044  issubg4  14638  gexcl3  14898  lbsextlem2  15912  iincld  16776  opnnei  16857  cncnp2  17010  lmmo  17108  iuncon  17154  ptbasfi  17276  filuni  17580  isfcls  17704  fclsopn  17709  nrginvrcn  18202  lebnumlem3  18461  cfil3i  18695  caun0  18707  iscmet3  18719  nulmbl2  18894  dyadmax  18953  itg2seq  19097  itg2monolem1  19105  rolle  19337  c1lip1  19344  taylfval  19738  ulm0  19770  isgrp2d  20902  cvmliftlem15  23829  dfon2lem6  24144  r19.2zr  24957  rexlimib  24959  lvsovso3  25628  filnetlem4  26330  filbcmb  26432  incsequz  26458  isbnd2  26507  isbnd3  26508  ssbnd  26512  unichnidl  26656  bnj906  28962
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-v 2790  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator