Theorem r19.2z 4012

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1879). 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 2901	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1810	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 206	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 3890	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 2902	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 284	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 445	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 383  ∀wal 1473  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-v 3175  df-dif 3543  df-nul 3875

This theorem is referenced by:  r19.2zb  4013  intssuni  4434  riinn0  4531  trintss  4697  iinexg  4751  reusv2lem2  4795  reusv2lem2OLD  4796  reusv2lem3  4797  xpiindi  5179  cnviin  5589  eusvobj2  6542  iiner  7706  finsschain  8156  cfeq0  8961  cfsuc  8962  iundom2g  9241  alephval2  9273  prlem934  9734  supaddc  10867  supadd  10868  supmul1  10869  supmullem2  10871  supmul  10872  rexfiuz  13935  r19.2uz  13939  climuni  14131  caurcvg  14255  caurcvg2  14256  caucvg  14257  pc2dvds  15421  vdwmc2  15521  vdwlem6  15528  vdwnnlem3  15539  issubg4  17436  gexcl3  17825  lbsextlem2  18980  iincld  20653  opnnei  20734  cncnp2  20895  lmmo  20994  iuncon  21041  ptbasfi  21194  filuni  21499  isfcls  21623  fclsopn  21628  ustfilxp  21826  nrginvrcn  22306  lebnumlem3  22570  cfil3i  22875  caun0  22887  iscmet3  22899  nulmbl2  23111  dyadmax  23172  itg2seq  23315  itg2monolem1  23323  rolle  23557  c1lip1  23564  taylfval  23917  ulm0  23949  usgreghash2spot  26596  bnj906  30254  cvmliftlem15  30534  dfon2lem6  30937  filnetlem4  31546  itg2addnclem  32631  itg2addnc  32634  itg2gt0cn  32635  bddiblnc  32650  ftc1anc  32663  filbcmb  32705  incsequz  32714  isbnd2  32752  isbnd3  32753  ssbnd  32757  unichnidl  33000  iunconlem2  38193  upbdrech  38460  fusgreghash2wsp  41502  av-frgrareg  41548