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

Theorem r19.2z 3918
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1751). 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
Distinct variable group:   ,

Proof of Theorem r19.2z
StepHypRef Expression
1 df-ral 2812 . . . 4
2 exintr 1702 . . . 4
31, 2sylbi 195 . . 3
4 n0 3794 . . 3
5 df-rex 2813 . . 3
63, 4, 53imtr4g 270 . 2
76impcom 430 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  A.wal 1393  E.wex 1612  e.wcel 1818  =/=wne 2652  A.wral 2807  E.wrex 2808   c0 3784
This theorem is referenced by:  r19.2zb  3919  intssuni  4309  riinn0  4405  trintss  4561  iinexg  4612  reusv2lem2  4654  reusv2lem3  4655  reusv6OLD  4663  xpiindi  5143  cnviin  5549  eusvobj2  6289  iiner  7402  finsschain  7847  cfeq0  8657  cfsuc  8658  iundom2g  8936  alephval2  8968  prlem934  9432  supmul1  10533  supmullem2  10535  supmul  10536  rexfiuz  13180  r19.2uz  13184  climuni  13375  caurcvg  13499  caurcvg2  13500  caucvg  13501  pc2dvds  14402  vdwmc2  14497  vdwlem6  14504  vdwnnlem3  14515  issubg4  16220  gexcl3  16607  lbsextlem2  17805  iincld  19540  opnnei  19621  cncnp2  19782  lmmo  19881  iuncon  19929  ptbasfi  20082  filuni  20386  isfcls  20510  fclsopn  20515  ustfilxp  20715  nrginvrcn  21200  lebnumlem3  21463  cfil3i  21708  caun0  21720  iscmet3  21732  nulmbl2  21947  dyadmax  22007  itg2seq  22149  itg2monolem1  22157  rolle  22391  c1lip1  22398  taylfval  22754  ulm0  22786  usgreghash2spot  25069  isgrp2d  25237  cvmliftlem15  28743  dfon2lem6  29220  supaddc  30041  supadd  30042  itg2addnclem  30066  itg2addnc  30069  itg2gt0cn  30070  bddiblnc  30085  ftc1anc  30098  filnetlem4  30199  filbcmb  30231  incsequz  30241  isbnd2  30279  isbnd3  30280  ssbnd  30284  unichnidl  30428  upbdrech  31505  iunconlem2  33735  bnj906  33988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-v 3111  df-dif 3478  df-nul 3785
  Copyright terms: Public domain W3C validator