Theorem r19.2z 4455

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568  ∃wex 1812   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-ne 2957  df-ral 3078  df-rex 3088  df-dif 3902  df-nul 4280

This theorem is used by:  r19.2zb  4456  intssuni  4930  iinssiun  4965  riinn0  5043  iinexg  5309  reusv2lem2  5361  reusv2lem3  5362  xpiindi  5812  cnviin  6289  eusvobj2  7412  iiner  8810  finsschain  9348  cfeq0  10334  cfsuc  10335  iundom2g  10624  alephval2  10657  prlem934  11118  supaddc  12284  supadd  12285  supmul1  12286  supmullem2  12288  supmul  12289  rexfiuz  15515  r19.2uz  15519  climuni  15719  caurcvg  15844  caurcvg2  15845  caucvg  15846  pc2dvds  17057  vdwmc2  17157  vdwlem6  17164  vdwnnlem3  17175  issubg4  19356  gexcl3  19801  lbsextlem2  21437  iincld  23357  opnnei  23438  cncnp2  23599  lmmo  23698  iunconn  23746  ptbasfi  23900  filuni  24204  isfcls  24328  fclsopn  24333  ustfilxp  24532  nrginvrcn  25011  lebnumlem3  25284  cfil3i  25590  caun0  25602  iscmet3  25614  nulmbl2  25857  dyadmax  25919  itg2seq  26063  itg2monolem1  26071  bddiblnc  26162  rolle  26310  c1lip1  26317  taylfval  26686  ulm0  26718  frgrreg  30995  bnj906  35560  cvmliftlem15  36063  dfon2lem6  36550  filnetlem4  37169  itg2addnclem  38589  itg2addnc  38592  itg2gt0cn  38593  ftc1anc  38619  filbcmb  38674  incsequz  38682  isbnd2  38717  isbnd3  38718  ssbnd  38722  unichnidl  38965  iunconnlem2  45916  upbdrech  46320  infxrpnf  46455  iuneqconst2  49932  iineqconst2  49933  iinxp  49940  iinfssc  50164  alsralrex  50907  alsraln0  50908