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  2381  exdistrf  2445  equvini  2453  euor2  2606  2moexv  2620  2moswapv  2622  2euexv  2624  2moex  2633  2euex  2634  2moswap  2637  2mo  2641  rspe  3225  ceqex  3615  intab  4938  eusv2nf  5345  copsexgw  5445  copsexg  5446  dmcosseq  5929  dmcosseqOLD  5930  dminss  6114  imainss  6115  relssdmrnOLD  6230  oprabidw  7400  oprabid  7401  frrlem8  8249  frrlem10  8251  hta  9826  axextnd  10520  axpowndlem2  10527  axregndlem1  10531  axregnd  10533  fpwwe  10575  reclem2pr  10977  bnj1121  34948  finminlem  36279  bj-19.23bit  36652  bj-nexrt  36653  bj-19.9htbi  36664  bj-sbsb  36798  bj-finsumval0  37246  wl-exeq  37495  mopickr  38318  ax12indn  38909  pm11.58  44352  axc11next  44368  iotavalsb  44395  vk15.4j  44491  onfrALTlem1  44511  onfrALTlem1VD  44852  vk15.4jVD  44876  suprnmpt  45141  ssfiunibd  45280  pgind  49679