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

Theorem r19.2z 3709
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 2702 . . . 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 3629 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2703 . . 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 2598   A.wral 2697   E.wrex 2698   (/)c0 3620
This theorem is referenced by:  r19.2zb  3710  intssuni  4064  riinn0  4157  trintss  4310  iinexg  4352  reusv2lem2  4717  reusv2lem3  4718  reusv6OLD  4726  xpiindi  5002  cnviin  5401  eusvobj2  6574  iiner  6968  finsschain  7405  cfeq0  8128  cfsuc  8129  iundom2g  8407  alephval2  8439  prlem934  8902  supmul1  9965  supmullem2  9967  supmul  9968  rexfiuz  12143  r19.2uz  12147  climuni  12338  caurcvg  12462  caurcvg2  12463  caucvg  12464  pc2dvds  13244  vdwmc2  13339  vdwlem6  13346  vdwnnlem3  13357  issubg4  14953  gexcl3  15213  lbsextlem2  16223  iincld  17095  opnnei  17176  cncnp2  17337  lmmo  17436  iuncon  17483  ptbasfi  17605  filuni  17909  isfcls  18033  fclsopn  18038  ustfilxp  18234  nrginvrcn  18719  lebnumlem3  18980  cfil3i  19214  caun0  19226  iscmet3  19238  nulmbl2  19423  dyadmax  19482  itg2seq  19626  itg2monolem1  19634  rolle  19866  c1lip1  19873  taylfval  20267  ulm0  20299  isgrp2d  21815  cvmliftlem15  24977  dfon2lem6  25407  supaddc  26228  supadd  26229  itg2addnclem  26246  itg2addnc  26249  itg2gt0cn  26250  bddiblnc  26265  ftc1anc  26278  filnetlem4  26401  filbcmb  26433  incsequz  26443  isbnd2  26483  isbnd3  26484  ssbnd  26488  unichnidl  26632  usgreghash2spot  28395  iunconlem2  28984  bnj906  29238
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-v 2950  df-dif 3315  df-nul 3621
  Copyright terms: Public domain W3C validator