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 1537  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

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

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  2383  exdistrf  2447  equvini  2455  sb1OLD  2482  euor2  2615  2moexv  2629  2moswapv  2631  2euexv  2633  2moex  2642  2euex  2643  2moswap  2646  2mo  2650  rspe  3237  ceqex  3582  intab  4909  eusv2nf  5318  copsexgw  5404  copsexg  5405  dmcosseq  5882  dminss  6056  imainss  6057  relssdmrn  6172  oprabidw  7306  oprabid  7307  frrlem8  8109  frrlem10  8111  hta  9655  axextnd  10347  axpowndlem2  10354  axregndlem1  10358  axregnd  10360  fpwwe  10402  reclem2pr  10804  bnj1121  32965  finminlem  34507  amosym1  34615  bj-19.23bit  34873  bj-nexrt  34874  bj-19.9htbi  34885  bj-sbsb  35020  bj-finsumval0  35456  wl-exeq  35693  ax12indn  36957  pm11.58  42008  axc11next  42024  iotavalsb  42051  vk15.4j  42148  onfrALTlem1  42168  onfrALTlem1VD  42510  vk15.4jVD  42534  suprnmpt  42710  ssfiunibd  42848