Theorem 19.8a 2182

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

Syntax hints:   → wi 4  ∀wal 1538  ∃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 1910  ax-6 1967  ax-7 2008  ax-12 2178

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

This theorem is referenced by:  19.8ad  2183  sp  2184  19.2g  2189  19.23bi  2192  nexr  2193  qexmid  2194  nf5r  2195  19.9t  2205  ax6e  2388  exdistrf  2452  equvini  2460  euor2  2613  2moexv  2627  2moswapv  2629  2euexv  2631  2moex  2640  2euex  2641  2moswap  2644  2mo  2648  rspe  3236  ceqex  3636  intab  4959  eusv2nf  5370  copsexgw  5470  copsexg  5471  dmcosseq  5961  dmcosseqOLD  5962  dminss  6147  imainss  6148  relssdmrnOLD  6263  oprabidw  7441  oprabid  7442  frrlem8  8297  frrlem10  8299  hta  9916  axextnd  10610  axpowndlem2  10617  axregndlem1  10621  axregnd  10623  fpwwe  10665  reclem2pr  11067  bnj1121  35021  finminlem  36341  bj-19.23bit  36714  bj-nexrt  36715  bj-19.9htbi  36726  bj-sbsb  36860  bj-finsumval0  37308  wl-exeq  37557  mopickr  38386  ax12indn  38966  pm11.58  44381  axc11next  44397  iotavalsb  44424  vk15.4j  44520  onfrALTlem1  44540  onfrALTlem1VD  44881  vk15.4jVD  44905  suprnmpt  45165  ssfiunibd  45305  pgind  49548