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

Theorem r19.2z 3717
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 2710 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1624 . . . 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 3637 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2711 . . 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 1549   E.wex 1550    e. wcel 1725    =/= wne 2599   A.wral 2705   E.wrex 2706   (/)c0 3628
This theorem is referenced by:  r19.2zb  3718  intssuni  4072  riinn0  4165  trintss  4318  iinexg  4360  reusv2lem2  4725  reusv2lem3  4726  reusv6OLD  4734  xpiindi  5010  cnviin  5409  eusvobj2  6582  iiner  6976  finsschain  7413  cfeq0  8136  cfsuc  8137  iundom2g  8415  alephval2  8447  prlem934  8910  supmul1  9973  supmullem2  9975  supmul  9976  rexfiuz  12151  r19.2uz  12155  climuni  12346  caurcvg  12470  caurcvg2  12471  caucvg  12472  pc2dvds  13252  vdwmc2  13347  vdwlem6  13354  vdwnnlem3  13365  issubg4  14961  gexcl3  15221  lbsextlem2  16231  iincld  17103  opnnei  17184  cncnp2  17345  lmmo  17444  iuncon  17491  ptbasfi  17613  filuni  17917  isfcls  18041  fclsopn  18046  ustfilxp  18242  nrginvrcn  18727  lebnumlem3  18988  cfil3i  19222  caun0  19234  iscmet3  19246  nulmbl2  19431  dyadmax  19490  itg2seq  19634  itg2monolem1  19642  rolle  19874  c1lip1  19881  taylfval  20275  ulm0  20307  isgrp2d  21823  cvmliftlem15  24985  dfon2lem6  25415  supaddc  26237  supadd  26238  itg2addnclem  26256  itg2addnc  26259  itg2gt0cn  26260  bddiblnc  26275  ftc1anc  26288  filnetlem4  26410  filbcmb  26442  incsequz  26452  isbnd2  26492  isbnd3  26493  ssbnd  26497  unichnidl  26641  usgreghash2spot  28458  iunconlem2  29047  bnj906  29301
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-v 2958  df-dif 3323  df-nul 3629
  Copyright terms: Public domain W3C validator