Theorem 19.8a 2189

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

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

This theorem is referenced by:  19.8ad  2190  sp  2191  19.2g  2196  19.23bi  2199  nexr  2200  qexmid  2201  nf5r  2202  19.9t  2212  ax6e  2387  exdistrf  2451  equvini  2459  euor2  2613  2moexv  2627  2moswapv  2629  2euexv  2631  2moex  2640  2euex  2641  2moswap  2644  2mo  2648  rspe  3227  ceqex  3594  intab  4920  eusv2nf  5337  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  dmcosseqOLD  5934  dmcosseqOLDOLD  5935  dminss  6117  imainss  6118  oprabidw  7398  oprabid  7399  frrlem8  8243  frrlem10  8245  hta  9821  axextnd  10514  axpowndlem2  10521  axregndlem1  10525  axregnd  10527  fpwwe  10569  reclem2pr  10971  bnj1121  35127  finminlem  36500  bj-19.23bit  36988  bj-nexrt  36989  bj-19.9htbi  37000  bj-sbsb  37144  bj-axreprepsep  37382  bj-finsumval0  37599  wl-exeq  37859  mopickr  38692  eldisjdmqsim  39138  ax12indn  39389  pm11.58  44817  axc11next  44833  iotavalsb  44860  vk15.4j  44955  onfrALTlem1  44975  onfrALTlem1VD  45316  vk15.4jVD  45340  suprnmpt  45604  ssfiunibd  45742  pgind  50192