Theorem 19.8a 2217

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

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

This theorem is used by:  19.8ad  2218  sp  2219  19.2g  2224  19.23bi  2227  nexr  2228  qexmid  2229  nf5r  2230  19.9t  2240  ax6e  2412  exdistrf  2476  equvini  2484  euor2  2638  2moexv  2652  2moswapv  2654  2euexv  2656  2moex  2665  2euex  2666  2moswap  2669  2mo  2673  rspe  3252  ceqex  3605  intab  4937  eusv2nf  5356  copsexgw  5459  copsexgwOLD  5460  copsexg  5461  cotsexgw  5462  dmcosseqOLD  5960  dminss  6142  imainss  6143  oprabidw  7452  oprabid  7453  frrlem8  8315  frrlem10  8317  hta  9966  htaOLD  9967  axextnd  10680  axpowndlem2  10687  axregndlem1  10691  axregnd  10693  fpwwe  10735  reclem2pr  11137  bnj1121  35662  finminlem  37199  bj-19.23bit  37686  bj-nexrt  37687  bj-19.9htbi  37698  bj-sbsb  37842  bj-axreprepsep  38084  bj-finsumval0  38300  wl-exeq  38560  mopickr  39397  eldisjdmqsim  39843  ax12indn  40094  pm11.58  45468  axc11next  45484  iotavalsb  45511  vk15.4j  45605  onfrALTlem1  45625  onfrALTlem1VD  45966  vk15.4jVD  45990  cocanss2  46016  suprnmpt  46283  ssfiunibd  46419  pgind  50979