Theorem r19.2z 4442

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 3048	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1893	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 217	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4300	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3057	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 407	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1539  ∃wex 1780   ∈ wcel 2111   ≠ wne 2928  ∀wral 3047  ∃wrex 3056  ∅c0 4280

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 2121  ax-ext 2703

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 2710  df-cleq 2723  df-ne 2929  df-ral 3048  df-rex 3057  df-dif 3900  df-nul 4281

This theorem is referenced by:  r19.2zb  4443  intssuni  4918  iinssiun  4953  riinn0  5029  iinexg  5284  reusv2lem2  5335  reusv2lem3  5336  xpiindi  5774  cnviin  6233  eusvobj2  7338  iiner  8713  finsschain  9243  cfeq0  10147  cfsuc  10148  iundom2g  10431  alephval2  10463  prlem934  10924  supaddc  12089  supadd  12090  supmul1  12091  supmullem2  12093  supmul  12094  rexfiuz  15255  r19.2uz  15259  climuni  15459  caurcvg  15584  caurcvg2  15585  caucvg  15586  pc2dvds  16791  vdwmc2  16891  vdwlem6  16898  vdwnnlem3  16909  issubg4  19058  gexcl3  19499  lbsextlem2  21096  iincld  22954  opnnei  23035  cncnp2  23196  lmmo  23295  iunconn  23343  ptbasfi  23496  filuni  23800  isfcls  23924  fclsopn  23929  ustfilxp  24128  nrginvrcn  24607  lebnumlem3  24889  cfil3i  25196  caun0  25208  iscmet3  25220  nulmbl2  25464  dyadmax  25526  itg2seq  25670  itg2monolem1  25678  bddiblnc  25770  rolle  25921  c1lip1  25929  taylfval  26293  ulm0  26327  frgrreg  30374  bnj906  34942  cvmliftlem15  35342  dfon2lem6  35830  filnetlem4  36423  itg2addnclem  37719  itg2addnc  37722  itg2gt0cn  37723  ftc1anc  37749  filbcmb  37788  incsequz  37796  isbnd2  37831  isbnd3  37832  ssbnd  37836  unichnidl  38079  iunconnlem2  44975  upbdrech  45354  infxrpnf  45492  iuneqconst2  48862  iineqconst2  48863  iinxp  48870  iinfssc  49097