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 4453
Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1981). 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 3066 . . . 4 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 exintr 1896 . . . 4 (∀𝑥(𝑥𝐴𝜑) → (∃𝑥 𝑥𝐴 → ∃𝑥(𝑥𝐴𝜑)))
31, 2sylbi 216 . . 3 (∀𝑥𝐴 𝜑 → (∃𝑥 𝑥𝐴 → ∃𝑥(𝑥𝐴𝜑)))
4 n0 4307 . . 3 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
5 df-rex 3075 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
63, 4, 53imtr4g 296 . 2 (∀𝑥𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥𝐴 𝜑))
76impcom 409 1 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝜑) → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wal 1540  wex 1782  wcel 2107  wne 2944  wral 3065  wrex 3074  c0 4283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-ne 2945  df-ral 3066  df-rex 3075  df-dif 3914  df-nul 4284
This theorem is referenced by:  r19.2zb  4454  intssuni  4932  iinssiun  4968  riinn0  5044  iinexg  5299  reusv2lem2  5355  reusv2lem3  5356  xpiindi  5792  cnviin  6239  eusvobj2  7350  iiner  8729  finsschain  9304  cfeq0  10193  cfsuc  10194  iundom2g  10477  alephval2  10509  prlem934  10970  supaddc  12123  supadd  12124  supmul1  12125  supmullem2  12127  supmul  12128  rexfiuz  15233  r19.2uz  15237  climuni  15435  caurcvg  15562  caurcvg2  15563  caucvg  15564  pc2dvds  16752  vdwmc2  16852  vdwlem6  16859  vdwnnlem3  16870  issubg4  18948  gexcl3  19370  lbsextlem2  20623  iincld  22393  opnnei  22474  cncnp2  22635  lmmo  22734  iunconn  22782  ptbasfi  22935  filuni  23239  isfcls  23363  fclsopn  23368  ustfilxp  23567  nrginvrcn  24059  lebnumlem3  24329  cfil3i  24636  caun0  24648  iscmet3  24660  nulmbl2  24903  dyadmax  24965  itg2seq  25110  itg2monolem1  25118  bddiblnc  25209  rolle  25357  c1lip1  25364  taylfval  25721  ulm0  25753  frgrreg  29341  bnj906  33545  cvmliftlem15  33895  dfon2lem6  34366  filnetlem4  34856  itg2addnclem  36132  itg2addnc  36135  itg2gt0cn  36136  ftc1anc  36162  filbcmb  36202  incsequz  36210  isbnd2  36245  isbnd3  36246  ssbnd  36250  unichnidl  36493  iunconnlem2  43224  upbdrech  43546  infxrpnf  43688
  Copyright terms: Public domain W3C validator