Theorem r19.2z 4439

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1978). 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 3052	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1894	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 217	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4293	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3062	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 407	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1540  ∃wex 1781   ∈ wcel 2114   ≠ wne 2932  ∀wral 3051  ∃wrex 3061  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-ne 2933  df-ral 3052  df-rex 3062  df-dif 3892  df-nul 4274

This theorem is referenced by:  r19.2zb  4440  intssuni  4912  iinssiun  4947  riinn0  5025  iinexg  5289  reusv2lem2  5341  reusv2lem3  5342  xpiindi  5790  cnviin  6250  eusvobj2  7359  iiner  8736  finsschain  9269  cfeq0  10178  cfsuc  10179  iundom2g  10462  alephval2  10495  prlem934  10956  supaddc  12123  supadd  12124  supmul1  12125  supmullem2  12127  supmul  12128  rexfiuz  15310  r19.2uz  15314  climuni  15514  caurcvg  15639  caurcvg2  15640  caucvg  15641  pc2dvds  16850  vdwmc2  16950  vdwlem6  16957  vdwnnlem3  16968  issubg4  19121  gexcl3  19562  lbsextlem2  21157  iincld  23004  opnnei  23085  cncnp2  23246  lmmo  23345  iunconn  23393  ptbasfi  23546  filuni  23850  isfcls  23974  fclsopn  23979  ustfilxp  24178  nrginvrcn  24657  lebnumlem3  24930  cfil3i  25236  caun0  25248  iscmet3  25260  nulmbl2  25503  dyadmax  25565  itg2seq  25709  itg2monolem1  25717  bddiblnc  25809  rolle  25957  c1lip1  25964  taylfval  26324  ulm0  26356  frgrreg  30464  bnj906  35072  cvmliftlem15  35480  dfon2lem6  35968  filnetlem4  36563  itg2addnclem  37992  itg2addnc  37995  itg2gt0cn  37996  ftc1anc  38022  filbcmb  38061  incsequz  38069  isbnd2  38104  isbnd3  38105  ssbnd  38109  unichnidl  38352  iunconnlem2  45361  upbdrech  45738  infxrpnf  45874  iuneqconst2  49298  iineqconst2  49299  iinxp  49306  iinfssc  49532