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

Theorem r19.2z 3910
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1718). 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 2812 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1673 . . . 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 3787 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2813 . . 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 1372   E.wex 1591    e. wcel 1762    =/= wne 2655   A.wral 2807   E.wrex 2808   (/)c0 3778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-v 3108  df-dif 3472  df-nul 3779
This theorem is referenced by:  r19.2zb  3911  intssuni  4297  riinn0  4393  trintss  4549  iinexg  4600  reusv2lem2  4642  reusv2lem3  4643  reusv6OLD  4651  xpiindi  5129  cnviin  5535  eusvobj2  6268  iiner  7373  finsschain  7816  cfeq0  8625  cfsuc  8626  iundom2g  8904  alephval2  8936  prlem934  9400  supmul1  10497  supmullem2  10499  supmul  10500  rexfiuz  13129  r19.2uz  13133  climuni  13324  caurcvg  13448  caurcvg2  13449  caucvg  13450  pc2dvds  14250  vdwmc2  14345  vdwlem6  14352  vdwnnlem3  14363  issubg4  16008  gexcl3  16396  lbsextlem2  17581  iincld  19299  opnnei  19380  cncnp2  19541  lmmo  19640  iuncon  19688  ptbasfi  19810  filuni  20114  isfcls  20238  fclsopn  20243  ustfilxp  20443  nrginvrcn  20928  lebnumlem3  21191  cfil3i  21436  caun0  21448  iscmet3  21460  nulmbl2  21675  dyadmax  21735  itg2seq  21877  itg2monolem1  21885  rolle  22119  c1lip1  22126  taylfval  22481  ulm0  22513  isgrp2d  24763  cvmliftlem15  28233  dfon2lem6  28647  supaddc  29468  supadd  29469  itg2addnclem  29494  itg2addnc  29497  itg2gt0cn  29498  bddiblnc  29513  ftc1anc  29526  filnetlem4  29653  filbcmb  29685  incsequz  29695  isbnd2  29733  isbnd3  29734  ssbnd  29738  unichnidl  29882  upbdrech  30901  usgreghash2spot  31788  iunconlem2  32690  bnj906  32942
  Copyright terms: Public domain W3C validator