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

Theorem r19.2z 3681
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 2675 . . . 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 3601 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2676 . . 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 2571   A.wral 2670   E.wrex 2671   (/)c0 3592
This theorem is referenced by:  r19.2zb  3682  intssuni  4036  riinn0  4129  trintss  4282  iinexg  4324  reusv2lem2  4688  reusv2lem3  4689  reusv6OLD  4697  xpiindi  4973  cnviin  5372  eusvobj2  6545  iiner  6939  finsschain  7375  cfeq0  8096  cfsuc  8097  iundom2g  8375  alephval2  8407  prlem934  8870  supmul1  9933  supmullem2  9935  supmul  9936  rexfiuz  12110  r19.2uz  12114  climuni  12305  caurcvg  12429  caurcvg2  12430  caucvg  12431  pc2dvds  13211  vdwmc2  13306  vdwlem6  13313  vdwnnlem3  13324  issubg4  14920  gexcl3  15180  lbsextlem2  16190  iincld  17062  opnnei  17143  cncnp2  17303  lmmo  17402  iuncon  17448  ptbasfi  17570  filuni  17874  isfcls  17998  fclsopn  18003  ustfilxp  18199  nrginvrcn  18684  lebnumlem3  18945  cfil3i  19179  caun0  19191  iscmet3  19203  nulmbl2  19388  dyadmax  19447  itg2seq  19591  itg2monolem1  19599  rolle  19831  c1lip1  19838  taylfval  20232  ulm0  20264  isgrp2d  21780  cvmliftlem15  24942  dfon2lem6  25362  supaddc  26141  supadd  26142  itg2addnclem  26159  itg2addnc  26162  itg2gt0cn  26163  bddiblnc  26178  filnetlem4  26304  filbcmb  26336  incsequz  26346  isbnd2  26386  isbnd3  26387  ssbnd  26391  unichnidl  26535  usgreghash2spot  28176  bnj906  29011
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 2389
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 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-v 2922  df-dif 3287  df-nul 3593
  Copyright terms: Public domain W3C validator