Theorem 19.8a 2175

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

Syntax hints:   → wi 4  ∀wal 1540  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  19.8ad  2176  sp  2177  19.2g  2182  19.23bi  2185  nexr  2186  qexmid  2187  nf5r  2188  19.9t  2198  ax6e  2383  exdistrf  2447  equvini  2455  euor2  2610  2moexv  2624  2moswapv  2626  2euexv  2628  2moex  2637  2euex  2638  2moswap  2641  2mo  2645  rspe  3247  ceqex  3641  intab  4983  eusv2nf  5394  copsexgw  5491  copsexg  5492  dmcosseq  5973  dminss  6153  imainss  6154  relssdmrnOLD  6269  oprabidw  7440  oprabid  7441  frrlem8  8278  frrlem10  8280  hta  9892  axextnd  10586  axpowndlem2  10593  axregndlem1  10597  axregnd  10599  fpwwe  10641  reclem2pr  11043  bnj1121  33996  finminlem  35203  bj-19.23bit  35569  bj-nexrt  35570  bj-19.9htbi  35581  bj-sbsb  35715  bj-finsumval0  36166  wl-exeq  36403  mopickr  37232  ax12indn  37813  pm11.58  43149  axc11next  43165  iotavalsb  43192  vk15.4j  43289  onfrALTlem1  43309  onfrALTlem1VD  43651  vk15.4jVD  43675  suprnmpt  43870  ssfiunibd  44019  pgind  47762