Theorem 19.8a 2176

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 2178. (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 2174	. . 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 1537  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

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

This theorem is referenced by:  19.8ad  2177  sp  2178  19.2g  2183  19.23bi  2186  nexr  2187  qexmid  2188  nf5r  2189  nf5rOLD  2190  19.9t  2200  ax6e  2383  exdistrf  2447  equvini  2455  sb1OLD  2482  euor2  2615  2moexv  2629  2moswapv  2631  2euexv  2633  2moex  2642  2euex  2643  2moswap  2646  2mo  2650  rspe  3232  ceqex  3574  intab  4906  eusv2nf  5313  copsexgw  5398  copsexg  5399  dmcosseq  5871  dminss  6045  imainss  6046  relssdmrn  6161  oprabidw  7286  oprabid  7287  frrlem8  8080  frrlem10  8082  hta  9586  axextnd  10278  axpowndlem2  10285  axregndlem1  10289  axregnd  10291  fpwwe  10333  reclem2pr  10735  bnj1121  32865  finminlem  34434  amosym1  34542  bj-19.23bit  34800  bj-nexrt  34801  bj-19.9htbi  34812  bj-sbsb  34947  bj-finsumval0  35383  wl-exeq  35620  ax12indn  36884  pm11.58  41897  axc11next  41913  iotavalsb  41940  vk15.4j  42037  onfrALTlem1  42057  onfrALTlem1VD  42399  vk15.4jVD  42423  suprnmpt  42599  ssfiunibd  42738