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  3219  ceqex  3609  intab  4931  eusv2nf  5337  copsexgw  5437  copsexg  5438  dmcosseqOLD  5924  dmcosseqOLDOLD  5925  dminss  6106  imainss  6107  oprabidw  7384  oprabid  7385  frrlem8  8233  frrlem10  8235  hta  9812  axextnd  10504  axpowndlem2  10511  axregndlem1  10515  axregnd  10517  fpwwe  10559  reclem2pr  10961  bnj1121  34954  finminlem  36294  bj-19.23bit  36667  bj-nexrt  36668  bj-19.9htbi  36679  bj-sbsb  36813  bj-finsumval0  37261  wl-exeq  37510  mopickr  38333  ax12indn  38924  pm11.58  44366  axc11next  44382  iotavalsb  44409  vk15.4j  44505  onfrALTlem1  44525  onfrALTlem1VD  44866  vk15.4jVD  44890  suprnmpt  45155  ssfiunibd  45294  pgind  49706