Theorem 19.8a 2188

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

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

This theorem is referenced by:  19.8ad  2189  sp  2190  19.2g  2195  19.23bi  2198  nexr  2199  qexmid  2200  nf5r  2201  19.9t  2211  ax6e  2387  exdistrf  2451  equvini  2459  euor2  2613  2moexv  2627  2moswapv  2629  2euexv  2631  2moex  2640  2euex  2641  2moswap  2644  2mo  2648  rspe  3226  ceqex  3606  intab  4933  eusv2nf  5340  copsexgw  5438  copsexg  5439  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  dminss  6111  imainss  6112  oprabidw  7389  oprabid  7390  frrlem8  8235  frrlem10  8237  hta  9809  axextnd  10502  axpowndlem2  10509  axregndlem1  10513  axregnd  10515  fpwwe  10557  reclem2pr  10959  bnj1121  35141  finminlem  36512  bj-19.23bit  36892  bj-nexrt  36893  bj-19.9htbi  36904  bj-sbsb  37038  bj-finsumval0  37490  wl-exeq  37739  mopickr  38556  ax12indn  39203  pm11.58  44631  axc11next  44647  iotavalsb  44674  vk15.4j  44769  onfrALTlem1  44789  onfrALTlem1VD  45130  vk15.4jVD  45154  suprnmpt  45418  ssfiunibd  45557  pgind  49962