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 1992 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 2180	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		alequexv 2012	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
3	1, 2	syl6 35	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
4		ax6evr 2027	. 2 ⊢ ∃𝑦 𝑥 = 𝑦
5	3, 4	exlimiiv 1938	1 ⊢ (𝜑 → ∃𝑥𝜑)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-12 2179

This theorem depends on definitions:  df-bi 210  df-ex 1787

This theorem is referenced by:  19.8ad  2183  sp  2184  19.2g  2189  19.23bi  2192  nexr  2193  qexmid  2194  nf5r  2195  nf5rOLD  2196  19.9t  2206  ax6e  2383  exdistrf  2447  equvini  2455  sb1OLD  2482  euor2  2616  2moexv  2630  2moswapv  2632  2euexv  2634  2moex  2643  2euex  2644  2moswap  2647  2mo  2651  rspe  3214  ceqex  3548  mo2icl  3613  intab  4866  eusv2nf  5262  copsexgw  5347  copsexg  5348  dmcosseq  5816  dminss  5985  imainss  5986  relssdmrn  6101  oprabidw  7201  oprabid  7202  hta  9399  axextnd  10091  axpowndlem2  10098  axregndlem1  10102  axregnd  10104  fpwwe  10146  reclem2pr  10548  bnj1121  32536  frrlem8  33448  frrlem10  33450  finminlem  34145  amosym1  34253  bj-19.23bit  34511  bj-nexrt  34512  bj-19.9htbi  34523  bj-sbsb  34651  bj-finsumval0  35077  wl-exeq  35316  ax12indn  36580  pm11.58  41546  axc11next  41562  iotavalsb  41589  vk15.4j  41686  onfrALTlem1  41706  onfrALTlem1VD  42048  vk15.4jVD  42072  suprnmpt  42248  ssfiunibd  42386