Theorem 19.8a 2178

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

Syntax hints:   → wi 4  ∀wal 1536  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175

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

This theorem is referenced by:  19.8ad  2179  sp  2180  19.2g  2185  19.23bi  2188  nexr  2189  qexmid  2190  nf5r  2191  nf5rOLD  2192  19.9t  2202  ax6e  2390  exdistrf  2458  equvini  2466  equviniOLD  2467  2ax6eOLD  2484  sb1OLD  2496  sbequ1ALT  2555  euor2  2674  2moexv  2689  2moswapv  2691  2euexv  2693  2moex  2702  2euex  2703  2moswap  2706  2mo  2710  rspe  3263  ceqex  3593  mo2icl  3653  intab  4868  eusv2nf  5261  copsexgw  5346  copsexg  5347  dmcosseq  5809  dminss  5977  imainss  5978  relssdmrn  6088  oprabidw  7166  oprabid  7167  hta  9310  axextnd  10002  axpowndlem2  10009  axregndlem1  10013  axregnd  10015  fpwwe  10057  reclem2pr  10459  bnj1121  32367  frrlem8  33243  frrlem10  33245  finminlem  33779  amosym1  33887  bj-19.23bit  34138  bj-nexrt  34139  bj-19.9htbi  34150  bj-sbsb  34275  bj-finsumval0  34700  wl-exeq  34939  ax12indn  36239  pm11.58  41094  axc11next  41110  iotavalsb  41137  vk15.4j  41234  onfrALTlem1  41254  onfrALTlem1VD  41596  vk15.4jVD  41620  suprnmpt  41798  ssfiunibd  41941