Theorem 19.8a 2223

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

Syntax hints:   → wi 4  ∀wal 1565  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-ex 1807

This theorem is referenced by:  19.8ad  2224  sp  2225  19.2g  2230  19.23bi  2233  nexr  2234  qexmid  2235  nf5r  2236  19.9t  2246  ax6e  2421  exdistrf  2485  equvini  2493  euor2  2647  2moexv  2661  2moswapv  2663  2euexv  2665  2moex  2674  2euex  2675  2moswap  2678  2mo  2682  rspe  3261  ceqex  3620  intab  4944  eusv2nf  5364  copsexgw  5470  copsexgwOLD  5471  copsexg  5472  dmcosseqOLD  5967  dminss  6148  imainss  6149  oprabidw  7439  oprabid  7440  frrlem8  8286  frrlem10  8288  hta  9879  axextnd  10572  axpowndlem2  10579  axregndlem1  10583  axregnd  10585  fpwwe  10627  reclem2pr  11029  bnj1121  35314  finminlem  36714  bj-19.23bit  37201  bj-nexrt  37202  bj-19.9htbi  37213  bj-sbsb  37357  bj-axreprepsep  37595  bj-finsumval0  37812  wl-exeq  38072  mopickr  38905  eldisjdmqsim  39351  ax12indn  39602  pm11.58  44987  axc11next  45003  iotavalsb  45030  vk15.4j  45124  onfrALTlem1  45144  onfrALTlem1VD  45485  vk15.4jVD  45509  suprnmpt  45779  ssfiunibd  45915  pgind  50375