Theorem 19.8a 2182

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

Syntax hints:   → wi 4  ∀wal 1535  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

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

This theorem is referenced by:  19.8ad  2183  sp  2184  19.2g  2189  19.23bi  2192  nexr  2193  qexmid  2194  nf5r  2195  19.9t  2205  ax6e  2391  exdistrf  2455  equvini  2463  euor2  2616  2moexv  2630  2moswapv  2632  2euexv  2634  2moex  2643  2euex  2644  2moswap  2647  2mo  2651  rspe  3255  ceqex  3665  intab  5002  eusv2nf  5413  copsexgw  5510  copsexg  5511  dmcosseq  5999  dmcosseqOLD  6000  dminss  6184  imainss  6185  relssdmrnOLD  6300  oprabidw  7479  oprabid  7480  frrlem8  8334  frrlem10  8336  hta  9966  axextnd  10660  axpowndlem2  10667  axregndlem1  10671  axregnd  10673  fpwwe  10715  reclem2pr  11117  bnj1121  34961  finminlem  36284  bj-19.23bit  36657  bj-nexrt  36658  bj-19.9htbi  36669  bj-sbsb  36803  bj-finsumval0  37251  wl-exeq  37488  mopickr  38319  ax12indn  38899  pm11.58  44359  axc11next  44375  iotavalsb  44402  vk15.4j  44499  onfrALTlem1  44519  onfrALTlem1VD  44861  vk15.4jVD  44885  suprnmpt  45081  ssfiunibd  45224  pgind  48809