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

Theorem r19.2z 3518
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 2523 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1616 . . . 4  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
31, 2sylbi 189 . . 3  |-  ( A. x  e.  A  ph  ->  ( E. x  x  e.  A  ->  E. x
( x  e.  A  /\  ph ) ) )
4 n0 3439 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2524 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
63, 4, 53imtr4g 263 . 2  |-  ( A. x  e.  A  ph  ->  ( A  =/=  (/)  ->  E. x  e.  A  ph ) )
76impcom 421 1  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360   A.wal 1532   E.wex 1537    e. wcel 1621    =/= wne 2421   A.wral 2518   E.wrex 2519   (/)c0 3430
This theorem is referenced by:  r19.2zb  3519  intssuni  3858  riinn0  3950  trintss  4103  iinexg  4147  reusv2lem2  4508  reusv2lem3  4509  reusv6OLD  4517  xpiindi  4809  cnviin  5199  eusvobj2  6305  iiner  6699  finsschain  7130  cfeq0  7850  cfsuc  7851  iundom2g  8130  alephval2  8162  prlem934  8625  supmul1  9687  supmullem2  9689  supmul  9690  rexfiuz  11797  r19.2uz  11801  climuni  11992  caurcvg  12115  caurcvg2  12116  caucvg  12117  pc2dvds  12894  vdwmc2  12989  vdwlem6  12996  vdwnnlem3  13007  issubg4  14601  gexcl3  14861  lbsextlem2  15875  iincld  16739  opnnei  16820  cncnp2  16973  lmmo  17071  iuncon  17117  ptbasfi  17239  filuni  17543  isfcls  17667  fclsopn  17672  nrginvrcn  18165  lebnumlem3  18424  cfil3i  18658  caun0  18670  iscmet3  18682  nulmbl2  18857  dyadmax  18916  itg2seq  19060  itg2monolem1  19068  rolle  19300  c1lip1  19307  taylfval  19701  ulm0  19733  isgrp2d  20863  cvmliftlem15  23202  dfon2lem6  23514  r19.2zr  24324  rexlimib  24326  lvsovso3  24996  filnetlem4  25698  filbcmb  25800  incsequz  25826  isbnd2  25875  isbnd3  25876  ssbnd  25880  unichnidl  26024  bnj906  28094
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-v 2765  df-dif 3130  df-nul 3431
  Copyright terms: Public domain W3C validator