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

Theorem r19.2z 3677
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1667). 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 2671 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1621 . . . 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 3597 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2672 . . 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 1546   E.wex 1547    e. wcel 1721    =/= wne 2567   A.wral 2666   E.wrex 2667   (/)c0 3588
This theorem is referenced by:  r19.2zb  3678  intssuni  4032  riinn0  4125  trintss  4278  iinexg  4320  reusv2lem2  4684  reusv2lem3  4685  reusv6OLD  4693  xpiindi  4969  cnviin  5368  eusvobj2  6541  iiner  6935  finsschain  7371  cfeq0  8092  cfsuc  8093  iundom2g  8371  alephval2  8403  prlem934  8866  supmul1  9929  supmullem2  9931  supmul  9932  rexfiuz  12106  r19.2uz  12110  climuni  12301  caurcvg  12425  caurcvg2  12426  caucvg  12427  pc2dvds  13207  vdwmc2  13302  vdwlem6  13309  vdwnnlem3  13320  issubg4  14916  gexcl3  15176  lbsextlem2  16186  iincld  17058  opnnei  17139  cncnp2  17299  lmmo  17398  iuncon  17444  ptbasfi  17566  filuni  17870  isfcls  17994  fclsopn  17999  ustfilxp  18195  nrginvrcn  18680  lebnumlem3  18941  cfil3i  19175  caun0  19187  iscmet3  19199  nulmbl2  19384  dyadmax  19443  itg2seq  19587  itg2monolem1  19595  rolle  19827  c1lip1  19834  taylfval  20228  ulm0  20260  isgrp2d  21776  cvmliftlem15  24938  dfon2lem6  25358  supaddc  26137  supadd  26138  itg2addnclem  26155  itg2addnc  26158  itg2gt0cn  26159  bddiblnc  26174  filnetlem4  26300  filbcmb  26332  incsequz  26342  isbnd2  26382  isbnd3  26383  ssbnd  26387  unichnidl  26531  usgreghash2spot  28172  bnj906  29007
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-v 2918  df-dif 3283  df-nul 3589
  Copyright terms: Public domain W3C validator