Theorem r19.2z 4458

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568  ∃wex 1812   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-ne 2960  df-ral 3081  df-rex 3091  df-dif 4050  df-nul 4282

This theorem is used by:  r19.2zb  4459  intssuni  4935  iinssiun  4970  riinn0  5048  iinexg  5316  reusv2lem2  5368  reusv2lem3  5369  xpiindi  5822  cnviin  6313  eusvobj2  7443  iiner  8848  finsschain  9386  cfeq0  10373  cfsuc  10374  iundom2g  10663  alephval2  10696  prlem934  11157  supaddc  12324  supadd  12325  supmul1  12326  supmullem2  12328  supmul  12329  rexfiuz  15559  r19.2uz  15563  climuni  15763  caurcvg  15888  caurcvg2  15889  caucvg  15890  pc2dvds  17101  vdwmc2  17201  vdwlem6  17208  vdwnnlem3  17219  issubg4  19406  gexcl3  19852  lbsextlem2  21488  iincld  23412  opnnei  23493  cncnp2  23654  lmmo  23753  iunconn  23801  ptbasfi  23955  filuni  24259  isfcls  24383  fclsopn  24388  ustfilxp  24587  nrginvrcn  25066  lebnumlem3  25339  cfil3i  25645  caun0  25657  iscmet3  25669  nulmbl2  25912  dyadmax  25974  itg2seq  26118  itg2monolem1  26126  bddiblnc  26217  rolle  26365  c1lip1  26372  taylfval  26743  ulm0  26775  frgrreg  31052  bnj906  35671  cvmliftlem15  36271  dfon2lem6  36765  filnetlem4  37384  itg2addnclem  38857  itg2addnc  38860  itg2gt0cn  38861  ftc1anc  38887  filbcmb  38940  incsequz  38948  isbnd2  38983  isbnd3  38984  ssbnd  38988  unichnidl  39231  iunconnlem2  46177  upbdrech  46594  infxrpnf  46729  iuneqconst2  50265  iineqconst2  50266  iinxp  50273  iinfssc  50502  alsralrex  51336  alsraln0  51337