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

Theorem r19.2z 3764
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1712). 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 2715 . . . 4  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 exintr 1668 . . . 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 3641 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
5 df-rex 2716 . . 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 1367   E.wex 1586    e. wcel 1756    =/= wne 2601   A.wral 2710   E.wrex 2711   (/)c0 3632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-v 2969  df-dif 3326  df-nul 3633
This theorem is referenced by:  r19.2zb  3765  intssuni  4145  riinn0  4240  trintss  4396  iinexg  4447  reusv2lem2  4489  reusv2lem3  4490  reusv6OLD  4498  xpiindi  4970  cnviin  5369  eusvobj2  6079  iiner  7164  finsschain  7610  cfeq0  8417  cfsuc  8418  iundom2g  8696  alephval2  8728  prlem934  9194  supmul1  10287  supmullem2  10289  supmul  10290  rexfiuz  12827  r19.2uz  12831  climuni  13022  caurcvg  13146  caurcvg2  13147  caucvg  13148  pc2dvds  13937  vdwmc2  14032  vdwlem6  14039  vdwnnlem3  14050  issubg4  15691  gexcl3  16077  lbsextlem2  17217  iincld  18618  opnnei  18699  cncnp2  18860  lmmo  18959  iuncon  19007  ptbasfi  19129  filuni  19433  isfcls  19557  fclsopn  19562  ustfilxp  19762  nrginvrcn  20247  lebnumlem3  20510  cfil3i  20755  caun0  20767  iscmet3  20779  nulmbl2  20993  dyadmax  21053  itg2seq  21195  itg2monolem1  21203  rolle  21437  c1lip1  21444  taylfval  21799  ulm0  21831  isgrp2d  23673  cvmliftlem15  27139  dfon2lem6  27552  supaddc  28370  supadd  28371  itg2addnclem  28396  itg2addnc  28399  itg2gt0cn  28400  bddiblnc  28415  ftc1anc  28428  filnetlem4  28555  filbcmb  28587  incsequz  28597  isbnd2  28635  isbnd3  28636  ssbnd  28640  unichnidl  28784  usgreghash2spot  30615  iunconlem2  31558  bnj906  31810
  Copyright terms: Public domain W3C validator