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

Theorem r19.2z 3485
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 2520 . . . 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 3406 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2521 . . 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 2419   A.wral 2516   E.wrex 2517   (/)c0 3397
This theorem is referenced by:  r19.2zb  3486  intssuni  3825  riinn0  3917  trintss  4069  iinexg  4113  reusv2lem2  4473  reusv2lem3  4474  reusv6OLD  4482  xpiindi  4774  cnviin  5164  eusvobj2  6270  iiner  6664  finsschain  7095  cfeq0  7815  cfsuc  7816  iundom2g  8095  alephval2  8127  prlem934  8590  supmul1  9652  supmullem2  9654  supmul  9655  rexfiuz  11761  r19.2uz  11765  climuni  11956  caurcvg  12079  caurcvg2  12080  caucvg  12081  pc2dvds  12858  vdwmc2  12953  vdwlem6  12960  vdwnnlem3  12971  issubg4  14565  gexcl3  14825  lbsextlem2  15839  iincld  16703  opnnei  16784  cncnp2  16937  lmmo  17035  iuncon  17081  ptbasfi  17203  filuni  17507  isfcls  17631  fclsopn  17636  nrginvrcn  18129  lebnumlem3  18388  cfil3i  18622  caun0  18634  iscmet3  18646  nulmbl2  18821  dyadmax  18880  itg2seq  19024  itg2monolem1  19032  rolle  19264  c1lip1  19271  taylfval  19665  ulm0  19697  isgrp2d  20827  cvmliftlem15  23166  dfon2lem6  23478  r19.2zr  24288  rexlimib  24290  lvsovso3  24960  filnetlem4  25662  filbcmb  25764  incsequz  25790  isbnd2  25839  isbnd3  25840  ssbnd  25844  unichnidl  25988  bnj906  27974
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-v 2742  df-dif 3097  df-nul 3398
  Copyright terms: Public domain W3C validator