Theorem 19.8a 2193

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

Syntax hints:   → wi 4  ∀wal 1545  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  19.8ad  2194  sp  2195  19.2g  2200  19.23bi  2203  nexr  2204  qexmid  2205  nf5r  2206  19.9t  2216  ax6e  2391  exdistrf  2455  equvini  2463  euor2  2617  2moexv  2631  2moswapv  2633  2euexv  2635  2moex  2644  2euex  2645  2moswap  2648  2mo  2652  rspe  3229  ceqex  3590  intab  4908  eusv2nf  5324  copsexgw  5430  copsexgwOLD  5431  copsexg  5432  dmcosseqOLD  5921  dmcosseqOLDOLD  5922  dminss  6104  imainss  6105  oprabidw  7387  oprabid  7388  frrlem8  8233  frrlem10  8235  hta  9812  axextnd  10505  axpowndlem2  10512  axregndlem1  10516  axregnd  10518  fpwwe  10560  reclem2pr  10962  bnj1121  35167  finminlem  36546  bj-19.23bit  37034  bj-nexrt  37035  bj-19.9htbi  37046  bj-sbsb  37190  bj-axreprepsep  37428  bj-finsumval0  37645  wl-exeq  37905  mopickr  38738  eldisjdmqsim  39184  ax12indn  39435  pm11.58  44834  axc11next  44850  iotavalsb  44877  vk15.4j  44972  onfrALTlem1  44992  onfrALTlem1VD  45333  vk15.4jVD  45357  suprnmpt  45621  ssfiunibd  45757  pgind  50207