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  7451  oprabid  7452  frrlem8  8311  frrlem10  8313  hta  9962  htaOLD  9963  axextnd  10676  axpowndlem2  10683  axregndlem1  10687  axregnd  10689  fpwwe  10731  reclem2pr  11133  bnj1121  35615  finminlem  37106  bj-19.23bit  37593  bj-nexrt  37594  bj-19.9htbi  37605  bj-sbsb  37749  bj-axreprepsep  37991  bj-finsumval0  38207  wl-exeq  38467  mopickr  39304  eldisjdmqsim  39750  ax12indn  40001  pm11.58  45374  axc11next  45390  iotavalsb  45417  vk15.4j  45511  onfrALTlem1  45531  onfrALTlem1VD  45872  vk15.4jVD  45896  cocanss2  45922  suprnmpt  46189  ssfiunibd  46325  pgind  50810