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

Theorem r19.2z 3449
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1759). 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 2513 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1616 . . . 4  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
31, 2sylbi 189 . . 3  |-  ( A. x  e.  A  ph  ->  ( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
4 n0 3371 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2514 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
63, 4, 53imtr4g 263 . 2  |-  ( A. x  e.  A  ph  ->  ( A  =/=  (/)  ->  E. x  e.  A  ph ) )
76impcom 421 1  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360   A.wal 1532   E.wex 1537    e. wcel 1621    =/= wne 2412   A.wral 2509   E.wrex 2510   (/)c0 3362
This theorem is referenced by:  r19.2zb  3450  intssuni  3782  riinn0  3874  trintss  4026  iinexg  4069  reusv2lem2  4427  reusv2lem3  4428  reusv6OLD  4436  xpiindi  4728  cnviin  5118  eusvobj2  6223  iiner  6617  finsschain  7046  cfeq0  7766  cfsuc  7767  iundom2g  8046  alephval2  8074  prlem934  8537  supmul1  9599  supmullem2  9601  supmul  9602  rexfiuz  11708  r19.2uz  11712  climuni  11903  caurcvg  12026  caurcvg2  12027  caucvg  12028  pc2dvds  12805  vdwmc2  12900  vdwlem6  12907  vdwnnlem3  12918  issubg4  14473  gexcl3  14733  lbsextlem2  15744  iincld  16608  opnnei  16689  cncnp2  16842  lmmo  16940  iuncon  16986  ptbasfi  17108  filuni  17412  isfcls  17536  fclsopn  17541  nrginvrcn  18034  lebnumlem3  18293  cfil3i  18527  caun0  18539  iscmet3  18551  nulmbl2  18726  dyadmax  18785  itg2seq  18929  itg2monolem1  18937  rolle  19169  c1lip1  19176  taylfval  19570  ulm0  19602  isgrp2d  20732  cvmliftlem15  23000  dfon2lem6  23312  r19.2zr  24122  rexlimib  24124  lvsovso3  24794  filnetlem4  25496  filbcmb  25598  incsequz  25624  isbnd2  25673  isbnd3  25674  ssbnd  25678  unichnidl  25822  bnj906  27651
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-v 2729  df-dif 3081  df-nul 3363
  Copyright terms: Public domain W3C validator