Theorem 19.8a 2174

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

Syntax hints:   → wi 4  ∀wal 1539  ∃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 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1782

This theorem is referenced by:  19.8ad  2175  sp  2176  19.2g  2181  19.23bi  2184  nexr  2185  qexmid  2186  nf5r  2187  19.9t  2197  ax6e  2381  exdistrf  2445  equvini  2453  euor2  2608  2moexv  2622  2moswapv  2624  2euexv  2626  2moex  2635  2euex  2636  2moswap  2639  2mo  2643  rspe  3245  ceqex  3636  intab  4975  eusv2nf  5386  copsexgw  5483  copsexg  5484  dmcosseq  5964  dminss  6141  imainss  6142  relssdmrnOLD  6257  oprabidw  7424  oprabid  7425  frrlem8  8260  frrlem10  8262  hta  9874  axextnd  10568  axpowndlem2  10575  axregndlem1  10579  axregnd  10581  fpwwe  10623  reclem2pr  11025  bnj1121  33825  finminlem  35005  bj-19.23bit  35371  bj-nexrt  35372  bj-19.9htbi  35383  bj-sbsb  35517  bj-finsumval0  35968  wl-exeq  36205  mopickr  37035  ax12indn  37616  pm11.58  42918  axc11next  42934  iotavalsb  42961  vk15.4j  43058  onfrALTlem1  43078  onfrALTlem1VD  43420  vk15.4jVD  43444  suprnmpt  43639  ssfiunibd  43790  pgind  47408