Theorem r19.2z 4500

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1973). 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 3059	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1889	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 217	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4358	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3068	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 407	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1534  ∃wex 1775   ∈ wcel 2105   ≠ wne 2937  ∀wral 3058  ∃wrex 3067  ∅c0 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-ne 2938  df-ral 3059  df-rex 3068  df-dif 3965  df-nul 4339

This theorem is referenced by:  r19.2zb  4501  intssuni  4974  iinssiun  5009  riinn0  5087  iinexg  5353  reusv2lem2  5404  reusv2lem3  5405  xpiindi  5848  cnviin  6307  eusvobj2  7422  iiner  8827  finsschain  9396  cfeq0  10293  cfsuc  10294  iundom2g  10577  alephval2  10609  prlem934  11070  supaddc  12232  supadd  12233  supmul1  12234  supmullem2  12236  supmul  12237  rexfiuz  15382  r19.2uz  15386  climuni  15584  caurcvg  15709  caurcvg2  15710  caucvg  15711  pc2dvds  16912  vdwmc2  17012  vdwlem6  17019  vdwnnlem3  17030  issubg4  19175  gexcl3  19619  lbsextlem2  21178  iincld  23062  opnnei  23143  cncnp2  23304  lmmo  23403  iunconn  23451  ptbasfi  23604  filuni  23908  isfcls  24032  fclsopn  24037  ustfilxp  24236  nrginvrcn  24728  lebnumlem3  25008  cfil3i  25316  caun0  25328  iscmet3  25340  nulmbl2  25584  dyadmax  25646  itg2seq  25791  itg2monolem1  25799  bddiblnc  25891  rolle  26042  c1lip1  26050  taylfval  26414  ulm0  26448  frgrreg  30422  bnj906  34922  cvmliftlem15  35282  dfon2lem6  35769  filnetlem4  36363  itg2addnclem  37657  itg2addnc  37660  itg2gt0cn  37661  ftc1anc  37687  filbcmb  37726  incsequz  37734  isbnd2  37769  isbnd3  37770  ssbnd  37774  unichnidl  38017  iunconnlem2  44932  upbdrech  45255  infxrpnf  45395