Theorem 19.8a 2220

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2216

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  19.8ad  2221  sp  2222  19.2g  2227  19.23bi  2230  nexr  2231  qexmid  2232  nf5r  2233  19.9t  2243  ax6e  2417  exdistrf  2481  equvini  2489  euor2  2643  2moexv  2657  2moswapv  2659  2euexv  2661  2moex  2670  2euex  2671  2moswap  2674  2mo  2678  rspe  3257  ceqex  3613  intab  4945  eusv2nf  5368  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  dmcosseqOLD  5971  dminss  6152  imainss  6153  oprabidw  7447  oprabid  7448  frrlem8  8292  frrlem10  8294  hta  9894  htaOLD  9895  axextnd  10587  axpowndlem2  10594  axregndlem1  10598  axregnd  10600  fpwwe  10642  reclem2pr  11044  bnj1121  35414  finminlem  36862  bj-19.23bit  37349  bj-nexrt  37350  bj-19.9htbi  37361  bj-sbsb  37505  bj-axreprepsep  37745  bj-finsumval0  37962  wl-exeq  38222  mopickr  39053  eldisjdmqsim  39499  ax12indn  39750  pm11.58  45133  axc11next  45149  iotavalsb  45176  vk15.4j  45270  onfrALTlem1  45290  onfrALTlem1VD  45631  vk15.4jVD  45655  suprnmpt  45925  ssfiunibd  46061  pgind  50528