Theorem r19.2z 4427

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1983). 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 3054	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1899	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 218	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4281	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3064	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 297	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 408	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1545  ∃wex 1786   ∈ wcel 2119   ≠ wne 2934  ∀wral 3053  ∃wrex 3063  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-ne 2935  df-ral 3054  df-rex 3064  df-dif 3886  df-nul 4262

This theorem is referenced by:  r19.2zb  4428  intssuni  4900  iinssiun  4935  riinn0  5012  iinexg  5276  reusv2lem2  5328  reusv2lem3  5329  xpiindi  5777  cnviin  6237  eusvobj2  7348  iiner  8726  finsschain  9259  cfeq0  10169  cfsuc  10170  iundom2g  10453  alephval2  10486  prlem934  10947  supaddc  12114  supadd  12115  supmul1  12116  supmullem2  12118  supmul  12119  rexfiuz  15301  r19.2uz  15305  climuni  15505  caurcvg  15630  caurcvg2  15631  caucvg  15632  pc2dvds  16841  vdwmc2  16941  vdwlem6  16948  vdwnnlem3  16959  issubg4  19112  gexcl3  19553  lbsextlem2  21152  iincld  23022  opnnei  23103  cncnp2  23264  lmmo  23363  iunconn  23411  ptbasfi  23564  filuni  23868  isfcls  23992  fclsopn  23997  ustfilxp  24196  nrginvrcn  24675  lebnumlem3  24948  cfil3i  25254  caun0  25266  iscmet3  25278  nulmbl2  25521  dyadmax  25583  itg2seq  25727  itg2monolem1  25735  bddiblnc  25827  rolle  25975  c1lip1  25982  taylfval  26342  ulm0  26374  frgrreg  30482  bnj906  35112  cvmliftlem15  35526  dfon2lem6  36014  filnetlem4  36609  itg2addnclem  38038  itg2addnc  38041  itg2gt0cn  38042  ftc1anc  38068  filbcmb  38107  incsequz  38115  isbnd2  38150  isbnd3  38151  ssbnd  38155  unichnidl  38398  iunconnlem2  45378  upbdrech  45753  infxrpnf  45889  iuneqconst2  49313  iineqconst2  49314  iinxp  49321  iinfssc  49547