Theorem r19.2z 4462

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 2009). 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 3082	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1925	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 220	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4307	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3092	. . 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 2146   ≠ wne 2960  ∀wral 3081  ∃wrex 3091  ∅c0 4286

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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-ne 2961  df-ral 3082  df-rex 3092  df-dif 3909  df-nul 4287

This theorem is used by:  r19.2zb  4463  intssuni  4937  iinssiun  4972  riinn0  5051  iinexg  5320  reusv2lem2  5372  reusv2lem3  5373  xpiindi  5823  cnviin  6291  eusvobj2  7411  iiner  8793  finsschain  9323  cfeq0  10255  cfsuc  10256  iundom2g  10539  alephval2  10572  prlem934  11033  supaddc  12197  supadd  12198  supmul1  12199  supmullem2  12201  supmul  12202  rexfiuz  15423  r19.2uz  15427  climuni  15627  caurcvg  15752  caurcvg2  15753  caucvg  15754  pc2dvds  16961  vdwmc2  17061  vdwlem6  17068  vdwnnlem3  17079  issubg4  19256  gexcl3  19701  lbsextlem2  21333  iincld  23246  opnnei  23327  cncnp2  23488  lmmo  23587  iunconn  23635  ptbasfi  23789  filuni  24093  isfcls  24217  fclsopn  24222  ustfilxp  24421  nrginvrcn  24900  lebnumlem3  25173  cfil3i  25479  caun0  25491  iscmet3  25503  nulmbl2  25746  dyadmax  25808  itg2seq  25952  itg2monolem1  25960  bddiblnc  26052  rolle  26200  c1lip1  26207  taylfval  26573  ulm0  26605  frgrreg  30816  bnj906  35383  cvmliftlem15  35827  dfon2lem6  36315  filnetlem4  36949  itg2addnclem  38379  itg2addnc  38382  itg2gt0cn  38383  ftc1anc  38409  filbcmb  38449  incsequz  38457  isbnd2  38492  isbnd3  38493  ssbnd  38497  unichnidl  38740  iunconnlem2  45701  upbdrech  46082  infxrpnf  46218  iuneqconst2  49658  iineqconst2  49659  iinxp  49666  iinfssc  49892  alsralrex  50647  alsraln0  50648