Theorem 19.8a 2189

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 1985 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2191. (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 2186	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		alequexv 2003	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
3	1, 2	syl6 35	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
4		ax6evr 2017	. 2 ⊢ ∃𝑦 𝑥 = 𝑦
5	3, 4	exlimiiv 1933	1 ⊢ (𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1540  ∃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 1912  ax-6 1969  ax-7 2010  ax-12 2185

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

This theorem is referenced by:  19.8ad  2190  sp  2191  19.2g  2196  19.23bi  2199  nexr  2200  qexmid  2201  nf5r  2202  19.9t  2212  ax6e  2388  exdistrf  2452  equvini  2460  euor2  2614  2moexv  2628  2moswapv  2630  2euexv  2632  2moex  2641  2euex  2642  2moswap  2645  2mo  2649  rspe  3228  ceqex  3595  intab  4921  eusv2nf  5330  copsexgw  5436  copsexg  5437  dmcosseqOLD  5926  dmcosseqOLDOLD  5927  dminss  6109  imainss  6110  oprabidw  7389  oprabid  7390  frrlem8  8234  frrlem10  8236  hta  9810  axextnd  10503  axpowndlem2  10510  axregndlem1  10514  axregnd  10516  fpwwe  10558  reclem2pr  10960  bnj1121  35133  finminlem  36506  bj-19.23bit  36986  bj-nexrt  36987  bj-19.9htbi  36998  bj-sbsb  37142  bj-axreprepsep  37380  bj-finsumval0  37597  wl-exeq  37850  mopickr  38683  eldisjdmqsim  39129  ax12indn  39380  pm11.58  44820  axc11next  44836  iotavalsb  44863  vk15.4j  44958  onfrALTlem1  44978  onfrALTlem1VD  45319  vk15.4jVD  45343  suprnmpt  45607  ssfiunibd  45745  pgind  50150