Theorem r19.2z 4461

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 3046	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		exintr 1892	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
3	1, 2	sylbi 217	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
4		n0 4319	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
5		df-rex 3055	. . 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 2926  ∀wral 3045  ∃wrex 3054  ∅c0 4299

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 2702

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 2709  df-cleq 2722  df-ne 2927  df-ral 3046  df-rex 3055  df-dif 3920  df-nul 4300

This theorem is referenced by:  r19.2zb  4462  intssuni  4937  iinssiun  4972  riinn0  5050  iinexg  5306  reusv2lem2  5357  reusv2lem3  5358  xpiindi  5802  cnviin  6262  eusvobj2  7382  iiner  8765  finsschain  9317  cfeq0  10216  cfsuc  10217  iundom2g  10500  alephval2  10532  prlem934  10993  supaddc  12157  supadd  12158  supmul1  12159  supmullem2  12161  supmul  12162  rexfiuz  15321  r19.2uz  15325  climuni  15525  caurcvg  15650  caurcvg2  15651  caucvg  15652  pc2dvds  16857  vdwmc2  16957  vdwlem6  16964  vdwnnlem3  16975  issubg4  19084  gexcl3  19524  lbsextlem2  21076  iincld  22933  opnnei  23014  cncnp2  23175  lmmo  23274  iunconn  23322  ptbasfi  23475  filuni  23779  isfcls  23903  fclsopn  23908  ustfilxp  24107  nrginvrcn  24587  lebnumlem3  24869  cfil3i  25176  caun0  25188  iscmet3  25200  nulmbl2  25444  dyadmax  25506  itg2seq  25650  itg2monolem1  25658  bddiblnc  25750  rolle  25901  c1lip1  25909  taylfval  26273  ulm0  26307  frgrreg  30330  bnj906  34927  cvmliftlem15  35292  dfon2lem6  35783  filnetlem4  36376  itg2addnclem  37672  itg2addnc  37675  itg2gt0cn  37676  ftc1anc  37702  filbcmb  37741  incsequz  37749  isbnd2  37784  isbnd3  37785  ssbnd  37789  unichnidl  38032  iunconnlem2  44931  upbdrech  45310  infxrpnf  45449  iuneqconst2  48815  iineqconst2  48816  iinxp  48823  iinfssc  49050