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

Theorem r19.2z 3870
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1714). 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 2800 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1669 . . . 4  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
31, 2sylbi 195 . . 3  |-  ( A. x  e.  A  ph  ->  ( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
4 n0 3747 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2801 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
63, 4, 53imtr4g 270 . 2  |-  ( A. x  e.  A  ph  ->  ( A  =/=  (/)  ->  E. x  e.  A  ph ) )
76impcom 430 1  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1368   E.wex 1587    e. wcel 1758    =/= wne 2644   A.wral 2795   E.wrex 2796   (/)c0 3738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-v 3073  df-dif 3432  df-nul 3739
This theorem is referenced by:  r19.2zb  3871  intssuni  4251  riinn0  4346  trintss  4502  iinexg  4553  reusv2lem2  4595  reusv2lem3  4596  reusv6OLD  4604  xpiindi  5076  cnviin  5475  eusvobj2  6186  iiner  7275  finsschain  7722  cfeq0  8529  cfsuc  8530  iundom2g  8808  alephval2  8840  prlem934  9306  supmul1  10399  supmullem2  10401  supmul  10402  rexfiuz  12946  r19.2uz  12950  climuni  13141  caurcvg  13265  caurcvg2  13266  caucvg  13267  pc2dvds  14056  vdwmc2  14151  vdwlem6  14158  vdwnnlem3  14169  issubg4  15811  gexcl3  16199  lbsextlem2  17355  iincld  18768  opnnei  18849  cncnp2  19010  lmmo  19109  iuncon  19157  ptbasfi  19279  filuni  19583  isfcls  19707  fclsopn  19712  ustfilxp  19912  nrginvrcn  20397  lebnumlem3  20660  cfil3i  20905  caun0  20917  iscmet3  20929  nulmbl2  21144  dyadmax  21204  itg2seq  21346  itg2monolem1  21354  rolle  21588  c1lip1  21595  taylfval  21950  ulm0  21982  isgrp2d  23867  cvmliftlem15  27324  dfon2lem6  27738  supaddc  28558  supadd  28559  itg2addnclem  28584  itg2addnc  28587  itg2gt0cn  28588  bddiblnc  28603  ftc1anc  28616  filnetlem4  28743  filbcmb  28775  incsequz  28785  isbnd2  28823  isbnd3  28824  ssbnd  28828  unichnidl  28972  usgreghash2spot  30803  iunconlem2  31974  bnj906  32226
  Copyright terms: Public domain W3C validator