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 2013 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 2214	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		alequexv 2031	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
3	1, 2	syl6 36	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
4		ax6evr 2045	. 2 ⊢ ∃𝑦 𝑥 = 𝑦
5	3, 4	exlimiiv 1961	1 ⊢ (𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1568  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  19.8ad  2218  sp  2219  19.2g  2224  19.23bi  2227  nexr  2228  qexmid  2229  nf5r  2230  19.9t  2240  ax6e  2415  exdistrf  2479  equvini  2487  euor2  2641  2moexv  2655  2moswapv  2657  2euexv  2659  2moex  2668  2euex  2669  2moswap  2672  2mo  2676  rspe  3255  ceqex  3611  intab  4943  eusv2nf  5366  copsexgw  5472  copsexgwOLD  5473  copsexg  5474  dmcosseqOLD  5969  dminss  6150  imainss  6151  oprabidw  7441  oprabid  7442  frrlem8  8286  frrlem10  8288  hta  9879  axextnd  10571  axpowndlem2  10578  axregndlem1  10582  axregnd  10584  fpwwe  10626  reclem2pr  11028  bnj1121  35373  finminlem  36829  bj-19.23bit  37316  bj-nexrt  37317  bj-19.9htbi  37328  bj-sbsb  37472  bj-axreprepsep  37712  bj-finsumval0  37929  wl-exeq  38189  mopickr  39020  eldisjdmqsim  39466  ax12indn  39717  pm11.58  45100  axc11next  45116  iotavalsb  45143  vk15.4j  45237  onfrALTlem1  45257  onfrALTlem1VD  45598  vk15.4jVD  45622  suprnmpt  45892  ssfiunibd  46028  pgind  50495