Theorem r19.2z 4493

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1978). 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 3060	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1893	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 216	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4345	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3069	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 295	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 406	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 394  ∀wal 1537  ∃wex 1779   ∈ wcel 2104   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  ∅c0 4321

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-ne 2939  df-ral 3060  df-rex 3069  df-dif 3950  df-nul 4322

This theorem is referenced by:  r19.2zb  4494  intssuni  4973  iinssiun  5009  riinn0  5085  iinexg  5340  reusv2lem2  5396  reusv2lem3  5397  xpiindi  5834  cnviin  6284  eusvobj2  7403  iiner  8785  finsschain  9361  cfeq0  10253  cfsuc  10254  iundom2g  10537  alephval2  10569  prlem934  11030  supaddc  12185  supadd  12186  supmul1  12187  supmullem2  12189  supmul  12190  rexfiuz  15298  r19.2uz  15302  climuni  15500  caurcvg  15627  caurcvg2  15628  caucvg  15629  pc2dvds  16816  vdwmc2  16916  vdwlem6  16923  vdwnnlem3  16934  issubg4  19061  gexcl3  19496  lbsextlem2  20917  iincld  22763  opnnei  22844  cncnp2  23005  lmmo  23104  iunconn  23152  ptbasfi  23305  filuni  23609  isfcls  23733  fclsopn  23738  ustfilxp  23937  nrginvrcn  24429  lebnumlem3  24709  cfil3i  25017  caun0  25029  iscmet3  25041  nulmbl2  25285  dyadmax  25347  itg2seq  25492  itg2monolem1  25500  bddiblnc  25591  rolle  25742  c1lip1  25749  taylfval  26107  ulm0  26139  frgrreg  29914  bnj906  34239  cvmliftlem15  34587  dfon2lem6  35064  filnetlem4  35569  itg2addnclem  36842  itg2addnc  36845  itg2gt0cn  36846  ftc1anc  36872  filbcmb  36911  incsequz  36919  isbnd2  36954  isbnd3  36955  ssbnd  36959  unichnidl  37202  iunconnlem2  43998  upbdrech  44313  infxrpnf  44454