Theorem 19.8a 2184

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 2186. (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 2181	. . 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 2180

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

This theorem is referenced by:  19.8ad  2185  sp  2186  19.2g  2191  19.23bi  2194  nexr  2195  qexmid  2196  nf5r  2197  19.9t  2207  ax6e  2383  exdistrf  2447  equvini  2455  euor2  2608  2moexv  2622  2moswapv  2624  2euexv  2626  2moex  2635  2euex  2636  2moswap  2639  2mo  2643  rspe  3222  ceqex  3602  intab  4923  eusv2nf  5328  copsexgw  5425  copsexg  5426  dmcosseqOLD  5913  dmcosseqOLDOLD  5914  dminss  6095  imainss  6096  oprabidw  7372  oprabid  7373  frrlem8  8218  frrlem10  8220  hta  9785  axextnd  10477  axpowndlem2  10484  axregndlem1  10488  axregnd  10490  fpwwe  10532  reclem2pr  10934  bnj1121  34989  finminlem  36352  bj-19.23bit  36725  bj-nexrt  36726  bj-19.9htbi  36737  bj-sbsb  36871  bj-finsumval0  37319  wl-exeq  37568  mopickr  38391  ax12indn  38982  pm11.58  44423  axc11next  44439  iotavalsb  44466  vk15.4j  44561  onfrALTlem1  44581  onfrALTlem1VD  44922  vk15.4jVD  44946  suprnmpt  45211  ssfiunibd  45350  pgind  49749