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

Theorem r19.2z 3544
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1672). 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 2549 . . . 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 3465 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2550 . . 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 1685    =/= wne 2447   A.wral 2544   E.wrex 2545   (/)c0 3456
This theorem is referenced by:  r19.2zb  3545  intssuni  3885  riinn0  3977  trintss  4130  iinexg  4174  reusv2lem2  4535  reusv2lem3  4536  reusv6OLD  4544  xpiindi  4820  cnviin  5210  eusvobj2  6333  iiner  6727  finsschain  7158  cfeq0  7878  cfsuc  7879  iundom2g  8158  alephval2  8190  prlem934  8653  supmul1  9715  supmullem2  9717  supmul  9718  rexfiuz  11827  r19.2uz  11831  climuni  12022  caurcvg  12145  caurcvg2  12146  caucvg  12147  pc2dvds  12927  vdwmc2  13022  vdwlem6  13029  vdwnnlem3  13040  issubg4  14634  gexcl3  14894  lbsextlem2  15908  iincld  16772  opnnei  16853  cncnp2  17006  lmmo  17104  iuncon  17150  ptbasfi  17272  filuni  17576  isfcls  17700  fclsopn  17705  nrginvrcn  18198  lebnumlem3  18457  cfil3i  18691  caun0  18703  iscmet3  18715  nulmbl2  18890  dyadmax  18949  itg2seq  19093  itg2monolem1  19101  rolle  19333  c1lip1  19340  taylfval  19734  ulm0  19766  isgrp2d  20896  cvmliftlem15  23236  dfon2lem6  23548  r19.2zr  24367  rexlimib  24369  lvsovso3  25039  filnetlem4  25741  filbcmb  25843  incsequz  25869  isbnd2  25918  isbnd3  25919  ssbnd  25923  unichnidl  26067  bnj906  28241
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
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 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-v 2791  df-dif 3156  df-nul 3457
  Copyright terms: Public domain W3C validator