Theorem 19.8a 2215

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

Syntax hints:   → wi 4  ∀wal 1557  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

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

This theorem is referenced by:  19.8ad  2216  sp  2217  19.2g  2222  19.23bi  2225  nexr  2226  qexmid  2227  nf5r  2228  19.9t  2238  ax6e  2413  exdistrf  2477  equvini  2485  euor2  2639  2moexv  2653  2moswapv  2655  2euexv  2657  2moex  2666  2euex  2667  2moswap  2670  2mo  2674  rspe  3251  ceqex  3610  intab  4933  eusv2nf  5349  copsexgw  5455  copsexgwOLD  5456  copsexg  5457  dmcosseqOLD  5951  dmcosseqOLDOLD  5952  dminss  6134  imainss  6135  oprabidw  7422  oprabid  7423  frrlem8  8268  frrlem10  8270  hta  9849  axextnd  10543  axpowndlem2  10550  axregndlem1  10554  axregnd  10556  fpwwe  10598  reclem2pr  11000  bnj1121  35241  finminlem  36639  bj-19.23bit  37127  bj-nexrt  37128  bj-19.9htbi  37139  bj-sbsb  37283  bj-axreprepsep  37521  bj-finsumval0  37738  wl-exeq  37998  mopickr  38831  eldisjdmqsim  39277  ax12indn  39528  pm11.58  44927  axc11next  44943  iotavalsb  44970  vk15.4j  45065  onfrALTlem1  45085  onfrALTlem1VD  45426  vk15.4jVD  45450  suprnmpt  45713  ssfiunibd  45849  pgind  50299