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 1983 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 2001	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
3	1, 2	syl6 35	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
4		ax6evr 2015	. 2 ⊢ ∃𝑦 𝑥 = 𝑦
5	3, 4	exlimiiv 1931	1 ⊢ (𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

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

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  2381  exdistrf  2445  equvini  2453  euor2  2606  2moexv  2620  2moswapv  2622  2euexv  2624  2moex  2633  2euex  2634  2moswap  2637  2mo  2641  rspe  3227  ceqex  3618  intab  4942  eusv2nf  5350  copsexgw  5450  copsexg  5451  dmcosseq  5940  dmcosseqOLD  5941  dminss  6126  imainss  6127  relssdmrnOLD  6242  oprabidw  7418  oprabid  7419  frrlem8  8272  frrlem10  8274  hta  9850  axextnd  10544  axpowndlem2  10551  axregndlem1  10555  axregnd  10557  fpwwe  10599  reclem2pr  11001  bnj1121  34975  finminlem  36306  bj-19.23bit  36679  bj-nexrt  36680  bj-19.9htbi  36691  bj-sbsb  36825  bj-finsumval0  37273  wl-exeq  37522  mopickr  38345  ax12indn  38936  pm11.58  44379  axc11next  44395  iotavalsb  44422  vk15.4j  44518  onfrALTlem1  44538  onfrALTlem1VD  44879  vk15.4jVD  44903  suprnmpt  45168  ssfiunibd  45307  pgind  49703