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

Theorem r19.2z 4495
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1976). 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:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem r19.2z
StepHypRef Expression
1 df-ral 3062 . . . 4 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 exintr 1892 . . . 4 (∀𝑥(𝑥𝐴𝜑) → (∃𝑥 𝑥𝐴 → ∃𝑥(𝑥𝐴𝜑)))
31, 2sylbi 217 . . 3 (∀𝑥𝐴 𝜑 → (∃𝑥 𝑥𝐴 → ∃𝑥(𝑥𝐴𝜑)))
4 n0 4353 . . 3 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
5 df-rex 3071 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
63, 4, 53imtr4g 296 . 2 (∀𝑥𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥𝐴 𝜑))
76impcom 407 1 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝜑) → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wal 1538  wex 1779  wcel 2108  wne 2940  wral 3061  wrex 3070  c0 4333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-ne 2941  df-ral 3062  df-rex 3071  df-dif 3954  df-nul 4334
This theorem is referenced by:  r19.2zb  4496  intssuni  4970  iinssiun  5005  riinn0  5083  iinexg  5348  reusv2lem2  5399  reusv2lem3  5400  xpiindi  5846  cnviin  6306  eusvobj2  7423  iiner  8829  finsschain  9399  cfeq0  10296  cfsuc  10297  iundom2g  10580  alephval2  10612  prlem934  11073  supaddc  12235  supadd  12236  supmul1  12237  supmullem2  12239  supmul  12240  rexfiuz  15386  r19.2uz  15390  climuni  15588  caurcvg  15713  caurcvg2  15714  caucvg  15715  pc2dvds  16917  vdwmc2  17017  vdwlem6  17024  vdwnnlem3  17035  issubg4  19163  gexcl3  19605  lbsextlem2  21161  iincld  23047  opnnei  23128  cncnp2  23289  lmmo  23388  iunconn  23436  ptbasfi  23589  filuni  23893  isfcls  24017  fclsopn  24022  ustfilxp  24221  nrginvrcn  24713  lebnumlem3  24995  cfil3i  25303  caun0  25315  iscmet3  25327  nulmbl2  25571  dyadmax  25633  itg2seq  25777  itg2monolem1  25785  bddiblnc  25877  rolle  26028  c1lip1  26036  taylfval  26400  ulm0  26434  frgrreg  30413  bnj906  34944  cvmliftlem15  35303  dfon2lem6  35789  filnetlem4  36382  itg2addnclem  37678  itg2addnc  37681  itg2gt0cn  37682  ftc1anc  37708  filbcmb  37747  incsequz  37755  isbnd2  37790  isbnd3  37791  ssbnd  37795  unichnidl  38038  iunconnlem2  44955  upbdrech  45317  infxrpnf  45457
  Copyright terms: Public domain W3C validator