Theorem 19.8a 2186

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

Syntax hints:   → wi 4  ∀wal 1539  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  19.8ad  2187  sp  2188  19.2g  2193  19.23bi  2196  nexr  2197  qexmid  2198  nf5r  2199  19.9t  2209  ax6e  2385  exdistrf  2449  equvini  2457  euor2  2610  2moexv  2624  2moswapv  2626  2euexv  2628  2moex  2637  2euex  2638  2moswap  2641  2mo  2645  rspe  3223  ceqex  3603  intab  4930  eusv2nf  5337  copsexgw  5435  copsexg  5436  dmcosseqOLD  5925  dmcosseqOLDOLD  5926  dminss  6108  imainss  6109  oprabidw  7386  oprabid  7387  frrlem8  8232  frrlem10  8234  hta  9801  axextnd  10493  axpowndlem2  10500  axregndlem1  10504  axregnd  10506  fpwwe  10548  reclem2pr  10950  bnj1121  35069  finminlem  36434  bj-19.23bit  36808  bj-nexrt  36809  bj-19.9htbi  36820  bj-sbsb  36954  bj-finsumval0  37402  wl-exeq  37651  mopickr  38468  ax12indn  39115  pm11.58  44547  axc11next  44563  iotavalsb  44590  vk15.4j  44685  onfrALTlem1  44705  onfrALTlem1VD  45046  vk15.4jVD  45070  suprnmpt  45334  ssfiunibd  45473  pgind  49878