Theorem r19.2z 4440

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1540  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ne 2934  df-ral 3053  df-rex 3063  df-dif 3893  df-nul 4275

This theorem is referenced by:  r19.2zb  4441  intssuni  4913  iinssiun  4948  riinn0  5026  iinexg  5285  reusv2lem2  5336  reusv2lem3  5337  xpiindi  5784  cnviin  6244  eusvobj2  7352  iiner  8729  finsschain  9262  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  21149  iincld  23014  opnnei  23095  cncnp2  23256  lmmo  23355  iunconn  23403  ptbasfi  23556  filuni  23860  isfcls  23984  fclsopn  23989  ustfilxp  24188  nrginvrcn  24667  lebnumlem3  24940  cfil3i  25246  caun0  25258  iscmet3  25270  nulmbl2  25513  dyadmax  25575  itg2seq  25719  itg2monolem1  25727  bddiblnc  25819  rolle  25967  c1lip1  25974  taylfval  26335  ulm0  26369  frgrreg  30479  bnj906  35088  cvmliftlem15  35496  dfon2lem6  35984  filnetlem4  36579  itg2addnclem  38006  itg2addnc  38009  itg2gt0cn  38010  ftc1anc  38036  filbcmb  38075  incsequz  38083  isbnd2  38118  isbnd3  38119  ssbnd  38123  unichnidl  38366  iunconnlem2  45379  upbdrech  45756  infxrpnf  45892  iuneqconst2  49310  iineqconst2  49311  iinxp  49318  iinfssc  49544