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  3608  intab  4935  eusv2nf  5342  copsexgw  5446  copsexg  5447  dmcosseqOLD  5936  dmcosseqOLDOLD  5937  dminss  6119  imainss  6120  oprabidw  7399  oprabid  7400  frrlem8  8245  frrlem10  8247  hta  9821  axextnd  10514  axpowndlem2  10521  axregndlem1  10525  axregnd  10527  fpwwe  10569  reclem2pr  10971  bnj1121  35160  finminlem  36531  bj-19.23bit  36933  bj-nexrt  36934  bj-19.9htbi  36945  bj-sbsb  37082  bj-axreprepsep  37320  bj-finsumval0  37537  wl-exeq  37786  mopickr  38619  eldisjdmqsim  39065  ax12indn  39316  pm11.58  44743  axc11next  44759  iotavalsb  44786  vk15.4j  44881  onfrALTlem1  44901  onfrALTlem1VD  45242  vk15.4jVD  45266  suprnmpt  45530  ssfiunibd  45668  pgind  50073