Theorem r19.2z 4458

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  ∅c0 4296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ne 2926  df-ral 3045  df-rex 3054  df-dif 3917  df-nul 4297

This theorem is referenced by:  r19.2zb  4459  intssuni  4934  iinssiun  4969  riinn0  5047  iinexg  5303  reusv2lem2  5354  reusv2lem3  5355  xpiindi  5799  cnviin  6259  eusvobj2  7379  iiner  8762  finsschain  9310  cfeq0  10209  cfsuc  10210  iundom2g  10493  alephval2  10525  prlem934  10986  supaddc  12150  supadd  12151  supmul1  12152  supmullem2  12154  supmul  12155  rexfiuz  15314  r19.2uz  15318  climuni  15518  caurcvg  15643  caurcvg2  15644  caucvg  15645  pc2dvds  16850  vdwmc2  16950  vdwlem6  16957  vdwnnlem3  16968  issubg4  19077  gexcl3  19517  lbsextlem2  21069  iincld  22926  opnnei  23007  cncnp2  23168  lmmo  23267  iunconn  23315  ptbasfi  23468  filuni  23772  isfcls  23896  fclsopn  23901  ustfilxp  24100  nrginvrcn  24580  lebnumlem3  24862  cfil3i  25169  caun0  25181  iscmet3  25193  nulmbl2  25437  dyadmax  25499  itg2seq  25643  itg2monolem1  25651  bddiblnc  25743  rolle  25894  c1lip1  25902  taylfval  26266  ulm0  26300  frgrreg  30323  bnj906  34920  cvmliftlem15  35285  dfon2lem6  35776  filnetlem4  36369  itg2addnclem  37665  itg2addnc  37668  itg2gt0cn  37669  ftc1anc  37695  filbcmb  37734  incsequz  37742  isbnd2  37777  isbnd3  37778  ssbnd  37782  unichnidl  38025  iunconnlem2  44924  upbdrech  45303  infxrpnf  45442  iuneqconst2  48811  iineqconst2  48812  iinxp  48819  iinfssc  49046