Theorem r19.2z 4460

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 2006). 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 3080	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1922	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 220	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4307	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3090	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 299	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 412	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 400  ∀wal 1568  ∃wex 1809   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-ne 2959  df-ral 3080  df-rex 3090  df-dif 3908  df-nul 4287

This theorem is referenced by:  r19.2zb  4461  intssuni  4935  iinssiun  4970  riinn0  5049  iinexg  5318  reusv2lem2  5370  reusv2lem3  5371  xpiindi  5821  cnviin  6287  eusvobj2  7402  iiner  8783  finsschain  9312  cfeq0  10235  cfsuc  10236  iundom2g  10519  alephval2  10552  prlem934  11013  supaddc  12177  supadd  12178  supmul1  12179  supmullem2  12181  supmul  12182  rexfiuz  15395  r19.2uz  15399  climuni  15599  caurcvg  15724  caurcvg2  15725  caucvg  15726  pc2dvds  16934  vdwmc2  17034  vdwlem6  17041  vdwnnlem3  17052  issubg4  19207  gexcl3  19652  lbsextlem2  21283  iincld  23196  opnnei  23277  cncnp2  23438  lmmo  23537  iunconn  23585  ptbasfi  23738  filuni  24042  isfcls  24166  fclsopn  24171  ustfilxp  24370  nrginvrcn  24849  lebnumlem3  25122  cfil3i  25428  caun0  25440  iscmet3  25452  nulmbl2  25695  dyadmax  25757  itg2seq  25901  itg2monolem1  25909  bddiblnc  26001  rolle  26149  c1lip1  26156  taylfval  26522  ulm0  26554  frgrreg  30745  bnj906  35318  cvmliftlem15  35790  dfon2lem6  36278  filnetlem4  36892  itg2addnclem  38322  itg2addnc  38325  itg2gt0cn  38326  ftc1anc  38352  filbcmb  38391  incsequz  38399  isbnd2  38434  isbnd3  38435  ssbnd  38439  unichnidl  38682  iunconnlem2  45643  upbdrech  46024  infxrpnf  46160  iuneqconst2  49601  iineqconst2  49602  iinxp  49609  iinfssc  49835  alsralrex  50590  alsraln0  50591