Theorem r19.2z 4454

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1567  ∃wex 1811   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  ∅c0 4277

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-ne 2956  df-ral 3077  df-rex 3087  df-dif 4046  df-nul 4278

This theorem is used by:  r19.2zb  4455  intssuni  4929  iinssiun  4964  riinn0  5042  iinexg  5309  reusv2lem2  5361  reusv2lem3  5362  xpiindi  5813  cnviin  6292  eusvobj2  7416  iiner  8817  finsschain  9355  cfeq0  10341  cfsuc  10342  iundom2g  10631  alephval2  10664  prlem934  11125  supaddc  12291  supadd  12292  supmul1  12293  supmullem2  12295  supmul  12296  rexfiuz  15524  r19.2uz  15528  climuni  15728  caurcvg  15853  caurcvg2  15854  caucvg  15855  pc2dvds  17066  vdwmc2  17166  vdwlem6  17173  vdwnnlem3  17184  issubg4  19365  gexcl3  19810  lbsextlem2  21446  iincld  23366  opnnei  23447  cncnp2  23608  lmmo  23707  iunconn  23755  ptbasfi  23909  filuni  24213  isfcls  24337  fclsopn  24342  ustfilxp  24541  nrginvrcn  25020  lebnumlem3  25293  cfil3i  25599  caun0  25611  iscmet3  25623  nulmbl2  25866  dyadmax  25928  itg2seq  26072  itg2monolem1  26080  bddiblnc  26171  rolle  26319  c1lip1  26326  taylfval  26695  ulm0  26727  frgrreg  31004  bnj906  35610  cvmliftlem15  36153  dfon2lem6  36646  filnetlem4  37265  itg2addnclem  38698  itg2addnc  38701  itg2gt0cn  38702  ftc1anc  38728  filbcmb  38783  incsequz  38791  isbnd2  38826  isbnd3  38827  ssbnd  38831  unichnidl  39074  iunconnlem2  46025  upbdrech  46429  infxrpnf  46564  iuneqconst2  50042  iineqconst2  50043  iinxp  50050  iinfssc  50279  alsralrex  51091  alsraln0  51092