Theorem 19.8a 2052

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 1895 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2053. (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 2048	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		ax6ev 1890	. . 3 ⊢ ∃𝑥 𝑥 = 𝑦
3		exim 1761	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥𝜑))
4	1, 2, 3	syl6mpi 67	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
5		ax6evr 1942	. 2 ⊢ ∃𝑦 𝑥 = 𝑦
6	4, 5	exlimiiv 1859	1 ⊢ (𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1481  ∃wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

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

This theorem is referenced by:  sp  2053  19.2g  2058  19.23bi  2061  nexr  2062  qexmid  2063  nf5r  2064  19.9t  2071  sbequ1  2110  19.9tOLD  2204  ax6e  2250  exdistrf  2333  equvini  2346  2ax6e  2450  euor2  2514  2moex  2543  2euex  2544  2moswap  2547  2mo  2551  rspe  3003  ceqex  3333  mo2icl  3385  intab  4507  eusv2nf  4864  copsexg  4956  dmcosseq  5387  dminss  5547  imainss  5548  relssdmrn  5656  oprabid  6677  hta  8760  domtriomlem  9264  axextnd  9413  axrepnd  9416  axunndlem1  9417  axunnd  9418  axpowndlem2  9420  axpownd  9423  axregndlem1  9424  axregnd  9426  axacndlem1  9429  axacndlem2  9430  axacndlem3  9431  axacndlem4  9432  axacndlem5  9433  axacnd  9434  fpwwe  9468  pwfseqlem4a  9483  pwfseqlem4  9484  reclem2pr  9870  bnj1121  31053  bnj1189  31077  finminlem  32312  amosym1  32425  bj-ssbft  32642  bj-19.23bit  32681  bj-nexrt  32682  bj-19.9htbi  32694  bj-sbsb  32824  bj-finsumval0  33147  isbasisrelowllem1  33203  isbasisrelowllem2  33204  wl-exeq  33321  ax12indn  34228  gneispace  38432  pm11.58  38590  axc11next  38607  iotavalsb  38634  vk15.4j  38734  onfrALTlem1  38763  onfrALTlem1VD  39126  vk15.4jVD  39150  suprnmpt  39355  ssfiunibd  39523  ovncvrrp  40778  19.8ad  42458