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 4401
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 3114 . . . 4 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 exintr 1893 . . . 4 (∀𝑥(𝑥𝐴𝜑) → (∃𝑥 𝑥𝐴 → ∃𝑥(𝑥𝐴𝜑)))
31, 2sylbi 220 . . 3 (∀𝑥𝐴 𝜑 → (∃𝑥 𝑥𝐴 → ∃𝑥(𝑥𝐴𝜑)))
4 n0 4263 . . 3 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
5 df-rex 3115 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
63, 4, 53imtr4g 299 . 2 (∀𝑥𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥𝐴 𝜑))
76impcom 411 1 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝜑) → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wal 1536  wex 1781  wcel 2112  wne 2990  wral 3109  wrex 3110  c0 4246
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ne 2991  df-ral 3114  df-rex 3115  df-dif 3887  df-nul 4247
This theorem is referenced by:  r19.2zb  4402  intssuni  4863  iinssiun  4897  riinn0  4971  iinexg  5211  reusv2lem2  5268  reusv2lem3  5269  xpiindi  5674  cnviin  6109  eusvobj2  7132  iiner  8356  finsschain  8819  cfeq0  9671  cfsuc  9672  iundom2g  9955  alephval2  9987  prlem934  10448  supaddc  11599  supadd  11600  supmul1  11601  supmullem2  11603  supmul  11604  rexfiuz  14702  r19.2uz  14706  climuni  14904  caurcvg  15028  caurcvg2  15029  caucvg  15030  pc2dvds  16208  vdwmc2  16308  vdwlem6  16315  vdwnnlem3  16326  issubg4  18293  gexcl3  18707  lbsextlem2  19927  iincld  21647  opnnei  21728  cncnp2  21889  lmmo  21988  iunconn  22036  ptbasfi  22189  filuni  22493  isfcls  22617  fclsopn  22622  ustfilxp  22821  nrginvrcn  23301  lebnumlem3  23571  cfil3i  23876  caun0  23888  iscmet3  23900  nulmbl2  24143  dyadmax  24205  itg2seq  24349  itg2monolem1  24357  bddiblnc  24448  rolle  24596  c1lip1  24603  taylfval  24957  ulm0  24989  frgrreg  28182  bnj906  32310  cvmliftlem15  32653  dfon2lem6  33141  filnetlem4  33837  itg2addnclem  35101  itg2addnc  35104  itg2gt0cn  35105  ftc1anc  35131  filbcmb  35171  incsequz  35179  isbnd2  35214  isbnd3  35215  ssbnd  35219  unichnidl  35462  iunconnlem2  41628  upbdrech  41924  infxrpnf  42071
  Copyright terms: Public domain W3C validator