Theorem 19.8a 2218

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  19.8ad  2219  sp  2220  19.2g  2225  19.23bi  2228  nexr  2229  qexmid  2230  nf5r  2231  19.9t  2241  ax6e  2413  exdistrf  2477  equvini  2485  euor2  2639  2moexv  2653  2moswapv  2655  2euexv  2657  2moex  2666  2euex  2667  2moswap  2670  2mo  2674  rspe  3253  ceqex  3606  intab  4938  eusv2nf  5357  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  cotsexgw  5463  dmcosseqOLD  5961  dminss  6143  imainss  6144  oprabidw  7449  oprabid  7450  frrlem8  8304  frrlem10  8306  hta  9955  htaOLD  9956  axextnd  10669  axpowndlem2  10676  axregndlem1  10680  axregnd  10682  fpwwe  10724  reclem2pr  11126  bnj1121  35608  finminlem  37086  bj-19.23bit  37573  bj-nexrt  37574  bj-19.9htbi  37585  bj-sbsb  37729  bj-axreprepsep  37971  bj-finsumval0  38186  wl-exeq  38446  mopickr  39283  eldisjdmqsim  39729  ax12indn  39980  pm11.58  45359  axc11next  45375  iotavalsb  45402  vk15.4j  45496  onfrALTlem1  45516  onfrALTlem1VD  45857  vk15.4jVD  45881  suprnmpt  46158  ssfiunibd  46294  pgind  50779