Theorem r19.2z 4422

Description: Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1981). 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 3068	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1896	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 216	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4277	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3069	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	3, 4, 5	3imtr4g 295	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝜑))
7	6	impcom 407	1 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1537  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-ne 2943  df-ral 3068  df-rex 3069  df-dif 3886  df-nul 4254

This theorem is referenced by:  r19.2zb  4423  intssuni  4898  iinssiun  4934  riinn0  5008  iinexg  5260  reusv2lem2  5317  reusv2lem3  5318  xpiindi  5733  cnviin  6178  eusvobj2  7248  iiner  8536  finsschain  9056  cfeq0  9943  cfsuc  9944  iundom2g  10227  alephval2  10259  prlem934  10720  supaddc  11872  supadd  11873  supmul1  11874  supmullem2  11876  supmul  11877  rexfiuz  14987  r19.2uz  14991  climuni  15189  caurcvg  15316  caurcvg2  15317  caucvg  15318  pc2dvds  16508  vdwmc2  16608  vdwlem6  16615  vdwnnlem3  16626  issubg4  18689  gexcl3  19107  lbsextlem2  20336  iincld  22098  opnnei  22179  cncnp2  22340  lmmo  22439  iunconn  22487  ptbasfi  22640  filuni  22944  isfcls  23068  fclsopn  23073  ustfilxp  23272  nrginvrcn  23762  lebnumlem3  24032  cfil3i  24338  caun0  24350  iscmet3  24362  nulmbl2  24605  dyadmax  24667  itg2seq  24812  itg2monolem1  24820  bddiblnc  24911  rolle  25059  c1lip1  25066  taylfval  25423  ulm0  25455  frgrreg  28659  bnj906  32810  cvmliftlem15  33160  dfon2lem6  33670  filnetlem4  34497  itg2addnclem  35755  itg2addnc  35758  itg2gt0cn  35759  ftc1anc  35785  filbcmb  35825  incsequz  35833  isbnd2  35868  isbnd3  35869  ssbnd  35873  unichnidl  36116  iunconnlem2  42444  upbdrech  42734  infxrpnf  42876