Theorem 19.8a 2172

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

Syntax hints:   → wi 4  ∀wal 1537  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-12 2169

This theorem depends on definitions:  df-bi 206  df-ex 1780

This theorem is referenced by:  19.8ad  2173  sp  2174  19.2g  2179  19.23bi  2182  nexr  2183  qexmid  2184  nf5r  2185  19.9t  2195  ax6e  2380  exdistrf  2444  equvini  2452  euor2  2607  2moexv  2621  2moswapv  2623  2euexv  2625  2moex  2634  2euex  2635  2moswap  2638  2mo  2642  rspe  3244  ceqex  3641  intab  4983  eusv2nf  5394  copsexgw  5491  copsexg  5492  dmcosseq  5973  dminss  6153  imainss  6154  relssdmrnOLD  6269  oprabidw  7444  oprabid  7445  frrlem8  8282  frrlem10  8284  hta  9896  axextnd  10590  axpowndlem2  10597  axregndlem1  10601  axregnd  10603  fpwwe  10645  reclem2pr  11047  bnj1121  34292  finminlem  35508  bj-19.23bit  35874  bj-nexrt  35875  bj-19.9htbi  35886  bj-sbsb  36020  bj-finsumval0  36471  wl-exeq  36708  mopickr  37537  ax12indn  38118  pm11.58  43453  axc11next  43469  iotavalsb  43496  vk15.4j  43593  onfrALTlem1  43613  onfrALTlem1VD  43955  vk15.4jVD  43979  suprnmpt  44173  ssfiunibd  44319  pgind  47851