Theorem 19.8a 2221

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 2018 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2223. (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 2217	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		alequexv 2036	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
3	1, 2	syl6 36	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
4		ax6evr 2050	. 2 ⊢ ∃𝑦 𝑥 = 𝑦
5	3, 4	exlimiiv 1966	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 1945  ax-6 2002  ax-7 2043  ax-12 2216

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

This theorem is used by:  19.8ad  2222  sp  2223  19.2g  2228  19.23bi  2231  nexr  2232  qexmid  2233  nf5r  2234  19.9t  2244  ax6e  2415  exdistrf  2479  equvini  2487  euor2  2641  2moexv  2655  2moswapv  2657  2euexv  2659  2moex  2668  2euex  2669  2moswap  2672  2mo  2676  rspe  3256  ceqex  3609  intab  4943  eusv2nf  5364  copsexgw  5467  copsexgwOLD  5468  copsexg  5469  cotsexgw  5470  dmcosseqOLD  5973  dminss  6161  imainss  6162  oprabidw  7482  oprabid  7483  frrlem8  8349  frrlem10  8351  hta  9999  htaOLD  10000  axextnd  10715  axpowndlem2  10722  axregndlem1  10726  axregnd  10728  fpwwe  10770  reclem2pr  11172  bnj1121  35726  finminlem  37321  bj-19.23bit  37808  bj-nexrt  37809  bj-19.9htbi  37820  bj-sbsb  37964  bj-axreprepsep  38261  bj-finsumval0  38474  wl-exeq  38734  mopickr  39569  eldisjdmqsim  40015  ax12indn  40266  pm11.58  45635  axc11next  45651  iotavalsb  45677  vk15.4j  45771  onfrALTlem1  45791  onfrALTlem1VD  46132  vk15.4jVD  46156  cocanss2  46183  suprnmpt  46462  ssfiunibd  46598  pgind  51216