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 3077	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1925	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 220	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4300	. . 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 1568  ∃wex 1812   ∈ wcel 2145   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  ∅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 2732

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 2739  df-cleq 2752  df-ne 2956  df-ral 3077  df-rex 3087  df-dif 3902  df-nul 4280

This theorem is used by:  r19.2zb  4456  intssuni  4930  iinssiun  4965  riinn0  5043  iinexg  5312  reusv2lem2  5364  reusv2lem3  5365  xpiindi  5815  cnviin  6284  eusvobj2  7405  iiner  8789  finsschain  9326  cfeq0  10258  cfsuc  10259  iundom2g  10548  alephval2  10581  prlem934  11042  supaddc  12206  supadd  12207  supmul1  12208  supmullem2  12210  supmul  12211  rexfiuz  15435  r19.2uz  15439  climuni  15639  caurcvg  15764  caurcvg2  15765  caucvg  15766  pc2dvds  16971  vdwmc2  17071  vdwlem6  17078  vdwnnlem3  17089  issubg4  19269  gexcl3  19714  lbsextlem2  21346  iincld  23264  opnnei  23345  cncnp2  23506  lmmo  23605  iunconn  23653  ptbasfi  23807  filuni  24111  isfcls  24235  fclsopn  24240  ustfilxp  24439  nrginvrcn  24918  lebnumlem3  25191  cfil3i  25497  caun0  25509  iscmet3  25521  nulmbl2  25764  dyadmax  25826  itg2seq  25970  itg2monolem1  25978  bddiblnc  26069  rolle  26217  c1lip1  26224  taylfval  26595  ulm0  26627  frgrreg  30874  bnj906  35439  cvmliftlem15  35877  dfon2lem6  36365  filnetlem4  37000  itg2addnclem  38420  itg2addnc  38423  itg2gt0cn  38424  ftc1anc  38450  filbcmb  38490  incsequz  38498  isbnd2  38533  isbnd3  38534  ssbnd  38538  unichnidl  38781  iunconnlem2  45757  upbdrech  46138  infxrpnf  46274  iuneqconst2  49751  iineqconst2  49752  iinxp  49759  iinfssc  49983  alsralrex  50741  alsraln0  50742