Theorem r19.2z 4354

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1958). 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

Step	Hyp	Ref	Expression
1		df-ral 3110	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1874	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 218	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4230	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3111	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 297	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 408	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1520  ∃wex 1761   ∈ wcel 2081   ≠ wne 2984  ∀wral 3105  ∃wrex 3106  ∅c0 4211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-dif 3862  df-nul 4212

This theorem is referenced by:  r19.2zb  4355  intssuni  4804  iinssiun  4837  riinn0  4904  iinexg  5135  reusv2lem2  5191  reusv2lem3  5192  xpiindi  5592  cnviin  6012  eusvobj2  7009  iiner  8219  finsschain  8677  cfeq0  9524  cfsuc  9525  iundom2g  9808  alephval2  9840  prlem934  10301  supaddc  11456  supadd  11457  supmul1  11458  supmullem2  11460  supmul  11461  rexfiuz  14541  r19.2uz  14545  climuni  14743  caurcvg  14867  caurcvg2  14868  caucvg  14869  pc2dvds  16044  vdwmc2  16144  vdwlem6  16151  vdwnnlem3  16162  issubg4  18052  gexcl3  18442  lbsextlem2  19621  iincld  21331  opnnei  21412  cncnp2  21573  lmmo  21672  iunconn  21720  ptbasfi  21873  filuni  22177  isfcls  22301  fclsopn  22306  ustfilxp  22504  nrginvrcn  22984  lebnumlem3  23250  cfil3i  23555  caun0  23567  iscmet3  23579  nulmbl2  23820  dyadmax  23882  itg2seq  24026  itg2monolem1  24034  rolle  24270  c1lip1  24277  taylfval  24630  ulm0  24662  frgrreg  27865  bnj906  31818  cvmliftlem15  32154  dfon2lem6  32642  filnetlem4  33339  itg2addnclem  34493  itg2addnc  34496  itg2gt0cn  34497  bddiblnc  34512  ftc1anc  34525  filbcmb  34566  incsequz  34574  isbnd2  34612  isbnd3  34613  ssbnd  34617  unichnidl  34860  iunconnlem2  40827  upbdrech  41132  infxrpnf  41282