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  5332  copsexgw  5438  copsexg  5439  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  dminss  6111  imainss  6112  oprabidw  7391  oprabid  7392  frrlem8  8236  frrlem10  8238  hta  9812  axextnd  10505  axpowndlem2  10512  axregndlem1  10516  axregnd  10518  fpwwe  10560  reclem2pr  10962  bnj1121  35143  finminlem  36516  bj-19.23bit  37004  bj-nexrt  37005  bj-19.9htbi  37016  bj-sbsb  37160  bj-axreprepsep  37398  bj-finsumval0  37615  wl-exeq  37873  mopickr  38706  eldisjdmqsim  39152  ax12indn  39403  pm11.58  44835  axc11next  44851  iotavalsb  44878  vk15.4j  44973  onfrALTlem1  44993  onfrALTlem1VD  45334  vk15.4jVD  45358  suprnmpt  45622  ssfiunibd  45760  pgind  50204