Theorem 19.8a 2217

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 2219. (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  2218  sp  2219  19.2g  2224  19.23bi  2227  nexr  2228  qexmid  2229  nf5r  2230  19.9t  2240  ax6e  2412  exdistrf  2476  equvini  2484  euor2  2638  2moexv  2652  2moswapv  2654  2euexv  2656  2moex  2665  2euex  2666  2moswap  2669  2mo  2673  rspe  3252  ceqex  3606  intab  4938  eusv2nf  5360  copsexgw  5466  copsexgwOLD  5467  copsexg  5468  dmcosseqOLD  5963  dminss  6144  imainss  6145  oprabidw  7444  oprabid  7445  frrlem8  8292  frrlem10  8294  hta  9901  htaOLD  9902  axextnd  10600  axpowndlem2  10607  axregndlem1  10611  axregnd  10613  fpwwe  10655  reclem2pr  11057  bnj1121  35494  finminlem  36937  bj-19.23bit  37424  bj-nexrt  37425  bj-19.9htbi  37436  bj-sbsb  37580  bj-axreprepsep  37820  bj-finsumval0  38037  wl-exeq  38297  mopickr  39119  eldisjdmqsim  39565  ax12indn  39816  pm11.58  45214  axc11next  45230  iotavalsb  45257  vk15.4j  45351  onfrALTlem1  45371  onfrALTlem1VD  45712  vk15.4jVD  45736  suprnmpt  46006  ssfiunibd  46142  pgind  50643