Theorem 19.8a 2174

Description: If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. See 19.8v 1986 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2176. (Revised by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 8-Dec-2019.)

Assertion

Ref	Expression
19.8a	⊢ (𝜑 → ∃𝑥𝜑)

Proof of Theorem 19.8a

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax12v 2172	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		alequexv 2004	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
3	1, 2	syl6 35	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
4		ax6evr 2018	. 2 ⊢ ∃𝑦 𝑥 = 𝑦
5	3, 4	exlimiiv 1934	1 ⊢ (𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1539  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1782

This theorem is referenced by:  19.8ad  2175  sp  2176  19.2g  2181  19.23bi  2184  nexr  2185  qexmid  2186  nf5r  2187  19.9t  2197  ax6e  2381  exdistrf  2445  equvini  2453  euor2  2608  2moexv  2622  2moswapv  2624  2euexv  2626  2moex  2635  2euex  2636  2moswap  2639  2mo  2643  rspe  3230  ceqex  3605  intab  4944  eusv2nf  5355  copsexgw  5452  copsexg  5453  dmcosseq  5933  dminss  6110  imainss  6111  relssdmrnOLD  6226  oprabidw  7393  oprabid  7394  frrlem8  8229  frrlem10  8231  hta  9842  axextnd  10536  axpowndlem2  10543  axregndlem1  10547  axregnd  10549  fpwwe  10591  reclem2pr  10993  bnj1121  33686  finminlem  34866  bj-19.23bit  35232  bj-nexrt  35233  bj-19.9htbi  35244  bj-sbsb  35378  bj-finsumval0  35829  wl-exeq  36066  mopickr  36897  ax12indn  37478  pm11.58  42792  axc11next  42808  iotavalsb  42835  vk15.4j  42932  onfrALTlem1  42952  onfrALTlem1VD  43294  vk15.4jVD  43318  suprnmpt  43513  ssfiunibd  43664  pgind  47282