Theorem 19.8a 2206

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 2064 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2207. (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 2204	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		ax6ev 2059	. . 3 ⊢ ∃𝑥 𝑥 = 𝑦
3		exim 1909	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥𝜑))
4	1, 2, 3	syl6mpi 67	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
5		ax6evr 2100	. 2 ⊢ ∃𝑦 𝑥 = 𝑦
6	4, 5	exlimiiv 2011	1 ⊢ (𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1629  ∃wex 1852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203

This theorem depends on definitions:  df-bi 197  df-ex 1853

This theorem is referenced by:  sp  2207  19.2g  2212  19.23bi  2215  nexr  2216  qexmid  2217  nf5r  2218  19.9t  2227  sbequ1  2266  19.9tOLD  2366  ax6e  2412  exdistrf  2483  equvini  2492  2ax6e  2598  euor2  2663  2moex  2692  2euex  2693  2moswap  2696  2mo  2700  rspe  3151  ceqex  3483  mo2icl  3537  intab  4641  eusv2nf  4995  copsexg  5083  dmcosseq  5525  dminss  5688  imainss  5689  relssdmrn  5800  oprabid  6822  hta  8924  domtriomlem  9466  axextnd  9615  axrepnd  9618  axunndlem1  9619  axunnd  9620  axpowndlem2  9622  axpownd  9625  axregndlem1  9626  axregnd  9628  axacndlem1  9631  axacndlem2  9632  axacndlem3  9633  axacndlem4  9634  axacndlem5  9635  axacnd  9636  fpwwe  9670  pwfseqlem4a  9685  pwfseqlem4  9686  reclem2pr  10072  bnj1121  31391  bnj1189  31415  frrlem11  32129  finminlem  32649  amosym1  32762  bj-ssbft  32979  bj-19.23bit  33018  bj-nexrt  33019  bj-19.9htbi  33031  bj-sbsb  33159  bj-finsumval0  33484  isbasisrelowllem1  33540  isbasisrelowllem2  33541  wl-exeq  33656  ax12indn  34751  gneispace  38958  pm11.58  39116  axc11next  39133  iotavalsb  39160  vk15.4j  39259  onfrALTlem1  39288  onfrALTlem1VD  39648  vk15.4jVD  39672  suprnmpt  39875  ssfiunibd  40040  ovncvrrp  41298  19.8ad  42989