Theorem 19.8a 2178

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

Syntax hints:   → wi 4  ∀wal 1534  ∃wex 1775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-12 2174

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

This theorem is referenced by:  19.8ad  2179  sp  2180  19.2g  2185  19.23bi  2188  nexr  2189  qexmid  2190  nf5r  2191  19.9t  2201  ax6e  2385  exdistrf  2449  equvini  2457  euor2  2610  2moexv  2624  2moswapv  2626  2euexv  2628  2moex  2637  2euex  2638  2moswap  2641  2mo  2645  rspe  3246  ceqex  3651  intab  4982  eusv2nf  5400  copsexgw  5500  copsexg  5501  dmcosseq  5989  dmcosseqOLD  5990  dminss  6174  imainss  6175  relssdmrnOLD  6290  oprabidw  7461  oprabid  7462  frrlem8  8316  frrlem10  8318  hta  9934  axextnd  10628  axpowndlem2  10635  axregndlem1  10639  axregnd  10641  fpwwe  10683  reclem2pr  11085  bnj1121  34977  finminlem  36300  bj-19.23bit  36673  bj-nexrt  36674  bj-19.9htbi  36685  bj-sbsb  36819  bj-finsumval0  37267  wl-exeq  37514  mopickr  38344  ax12indn  38924  pm11.58  44385  axc11next  44401  iotavalsb  44428  vk15.4j  44525  onfrALTlem1  44545  onfrALTlem1VD  44887  vk15.4jVD  44911  suprnmpt  45116  ssfiunibd  45259  pgind  48947