Theorem r19.2z 4470

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538  ∃wex 1779   ∈ wcel 2108   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  ∅c0 4308

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 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-ne 2933  df-ral 3052  df-rex 3061  df-dif 3929  df-nul 4309

This theorem is referenced by:  r19.2zb  4471  intssuni  4946  iinssiun  4981  riinn0  5059  iinexg  5318  reusv2lem2  5369  reusv2lem3  5370  xpiindi  5815  cnviin  6275  eusvobj2  7397  iiner  8803  finsschain  9371  cfeq0  10270  cfsuc  10271  iundom2g  10554  alephval2  10586  prlem934  11047  supaddc  12209  supadd  12210  supmul1  12211  supmullem2  12213  supmul  12214  rexfiuz  15366  r19.2uz  15370  climuni  15568  caurcvg  15693  caurcvg2  15694  caucvg  15695  pc2dvds  16899  vdwmc2  16999  vdwlem6  17006  vdwnnlem3  17017  issubg4  19128  gexcl3  19568  lbsextlem2  21120  iincld  22977  opnnei  23058  cncnp2  23219  lmmo  23318  iunconn  23366  ptbasfi  23519  filuni  23823  isfcls  23947  fclsopn  23952  ustfilxp  24151  nrginvrcn  24631  lebnumlem3  24913  cfil3i  25221  caun0  25233  iscmet3  25245  nulmbl2  25489  dyadmax  25551  itg2seq  25695  itg2monolem1  25703  bddiblnc  25795  rolle  25946  c1lip1  25954  taylfval  26318  ulm0  26352  frgrreg  30375  bnj906  34961  cvmliftlem15  35320  dfon2lem6  35806  filnetlem4  36399  itg2addnclem  37695  itg2addnc  37698  itg2gt0cn  37699  ftc1anc  37725  filbcmb  37764  incsequz  37772  isbnd2  37807  isbnd3  37808  ssbnd  37812  unichnidl  38055  iunconnlem2  44959  upbdrech  45334  infxrpnf  45473  iuneqconst2  48801  iineqconst2  48802  iinxp  48809  iinfssc  49024