Theorem r19.2z 4452

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1539  ∃wex 1780   ∈ wcel 2113   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-ne 2933  df-ral 3052  df-rex 3061  df-dif 3904  df-nul 4286

This theorem is referenced by:  r19.2zb  4453  intssuni  4925  iinssiun  4960  riinn0  5038  iinexg  5293  reusv2lem2  5344  reusv2lem3  5345  xpiindi  5784  cnviin  6244  eusvobj2  7350  iiner  8726  finsschain  9259  cfeq0  10166  cfsuc  10167  iundom2g  10450  alephval2  10483  prlem934  10944  supaddc  12109  supadd  12110  supmul1  12111  supmullem2  12113  supmul  12114  rexfiuz  15271  r19.2uz  15275  climuni  15475  caurcvg  15600  caurcvg2  15601  caucvg  15602  pc2dvds  16807  vdwmc2  16907  vdwlem6  16914  vdwnnlem3  16925  issubg4  19075  gexcl3  19516  lbsextlem2  21114  iincld  22983  opnnei  23064  cncnp2  23225  lmmo  23324  iunconn  23372  ptbasfi  23525  filuni  23829  isfcls  23953  fclsopn  23958  ustfilxp  24157  nrginvrcn  24636  lebnumlem3  24918  cfil3i  25225  caun0  25237  iscmet3  25249  nulmbl2  25493  dyadmax  25555  itg2seq  25699  itg2monolem1  25707  bddiblnc  25799  rolle  25950  c1lip1  25958  taylfval  26322  ulm0  26356  frgrreg  30469  bnj906  35086  cvmliftlem15  35492  dfon2lem6  35980  filnetlem4  36575  itg2addnclem  37872  itg2addnc  37875  itg2gt0cn  37876  ftc1anc  37902  filbcmb  37941  incsequz  37949  isbnd2  37984  isbnd3  37985  ssbnd  37989  unichnidl  38232  iunconnlem2  45175  upbdrech  45553  infxrpnf  45690  iuneqconst2  49068  iineqconst2  49069  iinxp  49076  iinfssc  49302