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  6288  eusvobj2  7410  iiner  8803  finsschain  9341  cfeq0  10327  cfsuc  10328  iundom2g  10617  alephval2  10650  prlem934  11111  supaddc  12277  supadd  12278  supmul1  12279  supmullem2  12281  supmul  12282  rexfiuz  15508  r19.2uz  15512  climuni  15712  caurcvg  15837  caurcvg2  15838  caucvg  15839  pc2dvds  17050  vdwmc2  17150  vdwlem6  17157  vdwnnlem3  17168  issubg4  19349  gexcl3  19794  lbsextlem2  21430  iincld  23350  opnnei  23431  cncnp2  23592  lmmo  23691  iunconn  23739  ptbasfi  23893  filuni  24197  isfcls  24321  fclsopn  24326  ustfilxp  24525  nrginvrcn  25004  lebnumlem3  25277  cfil3i  25583  caun0  25595  iscmet3  25607  nulmbl2  25850  dyadmax  25912  itg2seq  26056  itg2monolem1  26064  bddiblnc  26155  rolle  26303  c1lip1  26310  taylfval  26679  ulm0  26711  frgrreg  30988  bnj906  35553  cvmliftlem15  36042  dfon2lem6  36530  filnetlem4  37149  itg2addnclem  38569  itg2addnc  38572  itg2gt0cn  38573  ftc1anc  38599  filbcmb  38654  incsequz  38662  isbnd2  38697  isbnd3  38698  ssbnd  38702  unichnidl  38945  iunconnlem2  45902  upbdrech  46290  infxrpnf  46425  iuneqconst2  49902  iineqconst2  49903  iinxp  49910  iinfssc  50134  alsralrex  50877  alsraln0  50878