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

Theorem r19.2z 3834
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1759). 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 2737 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1710 . . . 4  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
31, 2sylbi 195 . . 3  |-  ( A. x  e.  A  ph  ->  ( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
4 n0 3721 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2738 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
63, 4, 53imtr4g 270 . 2  |-  ( A. x  e.  A  ph  ->  ( A  =/=  (/)  ->  E. x  e.  A  ph ) )
76impcom 428 1  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367   A.wal 1397   E.wex 1620    e. wcel 1826    =/= wne 2577   A.wral 2732   E.wrex 2733   (/)c0 3711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-v 3036  df-dif 3392  df-nul 3712
This theorem is referenced by:  r19.2zb  3835  intssuni  4222  riinn0  4318  trintss  4476  iinexg  4525  reusv2lem2  4567  reusv2lem3  4568  xpiindi  5051  cnviin  5453  eusvobj2  6189  iiner  7301  finsschain  7742  cfeq0  8549  cfsuc  8550  iundom2g  8828  alephval2  8860  prlem934  9322  supmul1  10424  supmullem2  10426  supmul  10427  rexfiuz  13182  r19.2uz  13186  climuni  13377  caurcvg  13501  caurcvg2  13502  caucvg  13503  pc2dvds  14404  vdwmc2  14499  vdwlem6  14506  vdwnnlem3  14517  issubg4  16337  gexcl3  16724  lbsextlem2  17918  iincld  19625  opnnei  19707  cncnp2  19868  lmmo  19967  iuncon  20014  ptbasfi  20167  filuni  20471  isfcls  20595  fclsopn  20600  ustfilxp  20800  nrginvrcn  21285  lebnumlem3  21548  cfil3i  21793  caun0  21805  iscmet3  21817  nulmbl2  22032  dyadmax  22092  itg2seq  22234  itg2monolem1  22242  rolle  22476  c1lip1  22483  taylfval  22839  ulm0  22871  usgreghash2spot  25190  isgrp2d  25354  cvmliftlem15  28932  dfon2lem6  29385  supaddc  30206  supadd  30207  itg2addnclem  30232  itg2addnc  30235  itg2gt0cn  30236  bddiblnc  30251  ftc1anc  30264  filnetlem4  30365  filbcmb  30397  incsequz  30407  isbnd2  30445  isbnd3  30446  ssbnd  30450  unichnidl  30594  upbdrech  31671  iunconlem2  34082  bnj906  34335
  Copyright terms: Public domain W3C validator