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

Syntax hints:   → wi 4  ∀wal 1531  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2173

This theorem depends on definitions:  df-bi 209  df-ex 1777

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  2397  exdistrf  2465  equvini  2473  equviniOLD  2474  2ax6eOLD  2491  sb1OLD  2503  sbequ1OLD  2516  sbequ1ALT  2575  euor2  2693  2moexv  2708  2moswapv  2710  2euexv  2712  2moex  2721  2euex  2722  2moswap  2725  2mo  2729  rspe  3304  ceqex  3644  mo2icl  3704  intab  4898  eusv2nf  5287  copsexgw  5373  copsexg  5374  dmcosseq  5838  dminss  6004  imainss  6005  relssdmrn  6115  oprabidw  7181  oprabid  7182  hta  9320  axextnd  10007  axpowndlem2  10014  axregndlem1  10018  axregnd  10020  fpwwe  10062  reclem2pr  10464  bnj1121  32252  frrlem8  33125  frrlem10  33127  finminlem  33661  amosym1  33769  bj-19.23bit  34020  bj-nexrt  34021  bj-19.9htbi  34032  bj-sbsb  34155  bj-finsumval0  34561  wl-exeq  34768  ax12indn  36073  pm11.58  40715  axc11next  40731  iotavalsb  40758  vk15.4j  40855  onfrALTlem1  40875  onfrALTlem1VD  41217  vk15.4jVD  41241  suprnmpt  41423  ssfiunibd  41569