Theorem r19.2z 4494

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

Step	Hyp	Ref	Expression
1		df-ral 3063	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1896	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 216	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4346	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3072	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 409	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 397  ∀wal 1540  ∃wex 1782   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  ∅c0 4322

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 2704

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 2711  df-cleq 2725  df-ne 2942  df-ral 3063  df-rex 3072  df-dif 3951  df-nul 4323

This theorem is referenced by:  r19.2zb  4495  intssuni  4974  iinssiun  5010  riinn0  5086  iinexg  5341  reusv2lem2  5397  reusv2lem3  5398  xpiindi  5834  cnviin  6283  eusvobj2  7398  iiner  8780  finsschain  9356  cfeq0  10248  cfsuc  10249  iundom2g  10532  alephval2  10564  prlem934  11025  supaddc  12178  supadd  12179  supmul1  12180  supmullem2  12182  supmul  12183  rexfiuz  15291  r19.2uz  15295  climuni  15493  caurcvg  15620  caurcvg2  15621  caucvg  15622  pc2dvds  16809  vdwmc2  16909  vdwlem6  16916  vdwnnlem3  16927  issubg4  19020  gexcl3  19450  lbsextlem2  20765  iincld  22535  opnnei  22616  cncnp2  22777  lmmo  22876  iunconn  22924  ptbasfi  23077  filuni  23381  isfcls  23505  fclsopn  23510  ustfilxp  23709  nrginvrcn  24201  lebnumlem3  24471  cfil3i  24778  caun0  24790  iscmet3  24802  nulmbl2  25045  dyadmax  25107  itg2seq  25252  itg2monolem1  25260  bddiblnc  25351  rolle  25499  c1lip1  25506  taylfval  25863  ulm0  25895  frgrreg  29637  bnj906  33930  cvmliftlem15  34278  dfon2lem6  34749  filnetlem4  35255  itg2addnclem  36528  itg2addnc  36531  itg2gt0cn  36532  ftc1anc  36558  filbcmb  36597  incsequz  36605  isbnd2  36640  isbnd3  36641  ssbnd  36645  unichnidl  36888  iunconnlem2  43682  upbdrech  44002  infxrpnf  44143