Theorem r19.2z 4453

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1996). 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 3077	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1912	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 219	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4305	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3087	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 298	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 411	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1558  ∃wex 1799   ∈ wcel 2142   ≠ wne 2957  ∀wral 3076  ∃wrex 3086  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-ne 2958  df-ral 3077  df-rex 3087  df-dif 3907  df-nul 4286

This theorem is referenced by:  r19.2zb  4454  intssuni  4928  iinssiun  4963  riinn0  5040  iinexg  5304  reusv2lem2  5356  reusv2lem3  5357  xpiindi  5807  cnviin  6273  eusvobj2  7388  iiner  8771  finsschain  9302  cfeq0  10213  cfsuc  10214  iundom2g  10497  alephval2  10530  prlem934  10991  supaddc  12159  supadd  12160  supmul1  12161  supmullem2  12163  supmul  12164  rexfiuz  15375  r19.2uz  15379  climuni  15579  caurcvg  15704  caurcvg2  15705  caucvg  15706  pc2dvds  16915  vdwmc2  17015  vdwlem6  17022  vdwnnlem3  17033  issubg4  19187  gexcl3  19627  lbsextlem2  21226  iincld  23096  opnnei  23177  cncnp2  23338  lmmo  23437  iunconn  23485  ptbasfi  23638  filuni  23942  isfcls  24066  fclsopn  24071  ustfilxp  24270  nrginvrcn  24749  lebnumlem3  25022  cfil3i  25328  caun0  25340  iscmet3  25352  nulmbl2  25595  dyadmax  25657  itg2seq  25801  itg2monolem1  25809  bddiblnc  25901  rolle  26049  c1lip1  26056  taylfval  26419  ulm0  26451  frgrreg  30593  bnj906  35222  cvmliftlem15  35645  dfon2lem6  36133  filnetlem4  36738  itg2addnclem  38167  itg2addnc  38170  itg2gt0cn  38171  ftc1anc  38197  filbcmb  38236  incsequz  38244  isbnd2  38279  isbnd3  38280  ssbnd  38284  unichnidl  38527  iunconnlem2  45507  upbdrech  45881  infxrpnf  46017  iuneqconst2  49441  iineqconst2  49442  iinxp  49449  iinfssc  49675