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

Theorem r19.2z 3900
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1736). 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 2796 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1687 . . . 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 3776 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2797 . . 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 430 1  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1379   E.wex 1597    e. wcel 1802    =/= wne 2636   A.wral 2791   E.wrex 2792   (/)c0 3767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-v 3095  df-dif 3461  df-nul 3768
This theorem is referenced by:  r19.2zb  3901  intssuni  4290  riinn0  4386  trintss  4542  iinexg  4593  reusv2lem2  4635  reusv2lem3  4636  reusv6OLD  4644  xpiindi  5124  cnviin  5530  eusvobj2  6270  iiner  7381  finsschain  7825  cfeq0  8634  cfsuc  8635  iundom2g  8913  alephval2  8945  prlem934  9409  supmul1  10509  supmullem2  10511  supmul  10512  rexfiuz  13154  r19.2uz  13158  climuni  13349  caurcvg  13473  caurcvg2  13474  caucvg  13475  pc2dvds  14274  vdwmc2  14369  vdwlem6  14376  vdwnnlem3  14387  issubg4  16089  gexcl3  16476  lbsextlem2  17673  iincld  19406  opnnei  19487  cncnp2  19648  lmmo  19747  iuncon  19795  ptbasfi  19948  filuni  20252  isfcls  20376  fclsopn  20381  ustfilxp  20581  nrginvrcn  21066  lebnumlem3  21329  cfil3i  21574  caun0  21586  iscmet3  21598  nulmbl2  21813  dyadmax  21873  itg2seq  22015  itg2monolem1  22023  rolle  22257  c1lip1  22264  taylfval  22619  ulm0  22651  usgreghash2spot  24934  isgrp2d  25102  cvmliftlem15  28609  dfon2lem6  29188  supaddc  30009  supadd  30010  itg2addnclem  30034  itg2addnc  30037  itg2gt0cn  30038  bddiblnc  30053  ftc1anc  30066  filnetlem4  30167  filbcmb  30199  incsequz  30209  isbnd2  30247  isbnd3  30248  ssbnd  30252  unichnidl  30396  upbdrech  31450  iunconlem2  33443  bnj906  33695
  Copyright terms: Public domain W3C validator