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

Theorem r19.2z 3892
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1801). 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 2787 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1749 . . . 4  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
31, 2sylbi 198 . . 3  |-  ( A. x  e.  A  ph  ->  ( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
4 n0 3777 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2788 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
63, 4, 53imtr4g 273 . 2  |-  ( A. x  e.  A  ph  ->  ( A  =/=  (/)  ->  E. x  e.  A  ph ) )
76impcom 431 1  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   A.wal 1435   E.wex 1659    e. wcel 1870    =/= wne 2625   A.wral 2782   E.wrex 2783   (/)c0 3767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-v 3089  df-dif 3445  df-nul 3768
This theorem is referenced by:  r19.2zb  3893  intssuni  4281  riinn0  4377  trintss  4536  iinexg  4585  reusv2lem2  4627  reusv2lem3  4628  xpiindi  4990  cnviin  5393  eusvobj2  6298  iiner  7443  finsschain  7887  cfeq0  8684  cfsuc  8685  iundom2g  8963  alephval2  8995  prlem934  9457  supaddc  10574  supadd  10575  supmul1  10576  supmullem2  10578  supmul  10579  rexfiuz  13389  r19.2uz  13393  climuni  13594  caurcvg  13720  caurcvgOLD  13721  caurcvg2  13722  caucvg  13723  pc2dvds  14782  vdwmc2  14883  vdwlem6  14890  vdwnnlem3  14901  issubg4  16778  gexcl3  17165  lbsextlem2  18308  iincld  19976  opnnei  20058  cncnp2  20219  lmmo  20318  iuncon  20365  ptbasfi  20518  filuni  20822  isfcls  20946  fclsopn  20951  ustfilxp  21149  nrginvrcn  21616  lebnumlem3  21878  cfil3i  22123  caun0  22135  iscmet3  22147  nulmbl2  22358  dyadmax  22424  itg2seq  22568  itg2monolem1  22576  rolle  22810  c1lip1  22817  taylfval  23170  ulm0  23202  usgreghash2spot  25633  isgrp2d  25799  bnj906  29520  cvmliftlem15  29800  dfon2lem6  30212  filnetlem4  30813  itg2addnclem  31687  itg2addnc  31690  itg2gt0cn  31691  bddiblnc  31706  ftc1anc  31719  filbcmb  31761  incsequz  31771  isbnd2  31809  isbnd3  31810  ssbnd  31814  unichnidl  31958  iunconlem2  36962  upbdrech  37122
  Copyright terms: Public domain W3C validator