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

Theorem r19.2z 3870
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1820). 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 2754 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1767 . . . 4  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
31, 2sylbi 200 . . 3  |-  ( A. x  e.  A  ph  ->  ( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
4 n0 3753 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2755 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
63, 4, 53imtr4g 278 . 2  |-  ( A. x  e.  A  ph  ->  ( A  =/=  (/)  ->  E. x  e.  A  ph ) )
76impcom 436 1  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375   A.wal 1453   E.wex 1674    e. wcel 1898    =/= wne 2633   A.wral 2749   E.wrex 2750   (/)c0 3743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-v 3059  df-dif 3419  df-nul 3744
This theorem is referenced by:  r19.2zb  3871  intssuni  4271  riinn0  4367  trintss  4529  iinexg  4580  reusv2lem2  4622  reusv2lem3  4623  xpiindi  4992  cnviin  5396  eusvobj2  6313  iiner  7466  finsschain  7912  cfeq0  8717  cfsuc  8718  iundom2g  8996  alephval2  9028  prlem934  9489  supaddc  10607  supadd  10608  supmul1  10609  supmullem2  10611  supmul  10612  rexfiuz  13465  r19.2uz  13469  climuni  13671  caurcvg  13797  caurcvgOLD  13798  caurcvg2  13799  caucvg  13800  pc2dvds  14883  vdwmc2  14984  vdwlem6  14991  vdwnnlem3  15002  issubg4  16891  gexcl3  17294  lbsextlem2  18437  iincld  20109  opnnei  20191  cncnp2  20352  lmmo  20451  iuncon  20498  ptbasfi  20651  filuni  20955  isfcls  21079  fclsopn  21084  ustfilxp  21282  nrginvrcn  21749  lebnumlem3  22046  lebnumlem3OLD  22049  cfil3i  22294  caun0  22306  iscmet3  22318  nulmbl2  22545  dyadmax  22612  itg2seq  22756  itg2monolem1  22764  rolle  22998  c1lip1  23005  taylfval  23370  ulm0  23402  usgreghash2spot  25853  isgrp2d  26019  bnj906  29791  cvmliftlem15  30071  dfon2lem6  30484  filnetlem4  31087  itg2addnclem  32039  itg2addnc  32042  itg2gt0cn  32043  bddiblnc  32058  ftc1anc  32071  filbcmb  32113  incsequz  32123  isbnd2  32161  isbnd3  32162  ssbnd  32166  unichnidl  32310  iunconlem2  37373  upbdrech  37598
  Copyright terms: Public domain W3C validator