Theorem r19.2z 4392

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

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1541  ∃wex 1787   ∈ wcel 2112   ≠ wne 2932  ∀wral 3051  ∃wrex 3052  ∅c0 4223

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-ne 2933  df-ral 3056  df-rex 3057  df-dif 3856  df-nul 4224

This theorem is referenced by:  r19.2zb  4393  intssuni  4867  iinssiun  4903  riinn0  4977  iinexg  5219  reusv2lem2  5277  reusv2lem3  5278  xpiindi  5689  cnviin  6129  eusvobj2  7184  iiner  8449  finsschain  8961  cfeq0  9835  cfsuc  9836  iundom2g  10119  alephval2  10151  prlem934  10612  supaddc  11764  supadd  11765  supmul1  11766  supmullem2  11768  supmul  11769  rexfiuz  14876  r19.2uz  14880  climuni  15078  caurcvg  15205  caurcvg2  15206  caucvg  15207  pc2dvds  16395  vdwmc2  16495  vdwlem6  16502  vdwnnlem3  16513  issubg4  18516  gexcl3  18930  lbsextlem2  20150  iincld  21890  opnnei  21971  cncnp2  22132  lmmo  22231  iunconn  22279  ptbasfi  22432  filuni  22736  isfcls  22860  fclsopn  22865  ustfilxp  23064  nrginvrcn  23544  lebnumlem3  23814  cfil3i  24120  caun0  24132  iscmet3  24144  nulmbl2  24387  dyadmax  24449  itg2seq  24594  itg2monolem1  24602  bddiblnc  24693  rolle  24841  c1lip1  24848  taylfval  25205  ulm0  25237  frgrreg  28431  bnj906  32577  cvmliftlem15  32927  dfon2lem6  33434  filnetlem4  34256  itg2addnclem  35514  itg2addnc  35517  itg2gt0cn  35518  ftc1anc  35544  filbcmb  35584  incsequz  35592  isbnd2  35627  isbnd3  35628  ssbnd  35632  unichnidl  35875  iunconnlem2  42169  upbdrech  42458  infxrpnf  42601