Theorem r19.2z 4450

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1539  ∃wex 1780   ∈ wcel 2113   ≠ wne 2930  ∀wral 3049  ∃wrex 3058  ∅c0 4283

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 2123  ax-ext 2706

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 2713  df-cleq 2726  df-ne 2931  df-ral 3050  df-rex 3059  df-dif 3902  df-nul 4284

This theorem is referenced by:  r19.2zb  4451  intssuni  4923  iinssiun  4958  riinn0  5036  iinexg  5291  reusv2lem2  5342  reusv2lem3  5343  xpiindi  5782  cnviin  6242  eusvobj2  7348  iiner  8724  finsschain  9257  cfeq0  10164  cfsuc  10165  iundom2g  10448  alephval2  10481  prlem934  10942  supaddc  12107  supadd  12108  supmul1  12109  supmullem2  12111  supmul  12112  rexfiuz  15269  r19.2uz  15273  climuni  15473  caurcvg  15598  caurcvg2  15599  caucvg  15600  pc2dvds  16805  vdwmc2  16905  vdwlem6  16912  vdwnnlem3  16923  issubg4  19073  gexcl3  19514  lbsextlem2  21112  iincld  22981  opnnei  23062  cncnp2  23223  lmmo  23322  iunconn  23370  ptbasfi  23523  filuni  23827  isfcls  23951  fclsopn  23956  ustfilxp  24155  nrginvrcn  24634  lebnumlem3  24916  cfil3i  25223  caun0  25235  iscmet3  25247  nulmbl2  25491  dyadmax  25553  itg2seq  25697  itg2monolem1  25705  bddiblnc  25797  rolle  25948  c1lip1  25956  taylfval  26320  ulm0  26354  frgrreg  30418  bnj906  35035  cvmliftlem15  35441  dfon2lem6  35929  filnetlem4  36524  itg2addnclem  37811  itg2addnc  37814  itg2gt0cn  37815  ftc1anc  37841  filbcmb  37880  incsequz  37888  isbnd2  37923  isbnd3  37924  ssbnd  37928  unichnidl  38171  iunconnlem2  45117  upbdrech  45495  infxrpnf  45632  iuneqconst2  49010  iineqconst2  49011  iinxp  49018  iinfssc  49244