MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.8a Structured version   Visualization version   GIF version

Theorem 19.8a 2039
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 1882 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2041. (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.
StepHypRef Expression
1 ax12v 2035 . . 3 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 ax6ev 1877 . . 3 𝑥 𝑥 = 𝑦
3 exim 1751 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥𝜑))
41, 2, 3syl6mpi 65 . 2 (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
5 ax6evr 1929 . 2 𝑦 𝑥 = 𝑦
64, 5exlimiiv 1846 1 (𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1473  wex 1695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034
This theorem depends on definitions:  df-bi 196  df-ex 1696
This theorem is referenced by:  sp  2041  19.2g  2046  19.23bi  2049  nexr  2050  qexmid  2051  nf5r  2052  19.9t  2059  sbequ1  2096  19.9tOLD  2192  ax6e  2238  exdistrf  2321  equvini  2334  2ax6e  2438  euor2  2502  2moex  2531  2euex  2532  2moswap  2535  2mo  2539  rspe  2986  ceqex  3303  mo2icl  3352  intab  4442  eusv2nf  4790  copsexg  4882  dmcosseq  5308  dminss  5466  imainss  5467  relssdmrn  5573  oprabid  6576  hta  8643  domtriomlem  9147  axextnd  9292  axrepnd  9295  axunndlem1  9296  axunnd  9297  axpowndlem2  9299  axpownd  9302  axregndlem1  9303  axregnd  9305  axacndlem1  9308  axacndlem2  9309  axacndlem3  9310  axacndlem4  9311  axacndlem5  9312  axacnd  9313  fpwwe  9347  pwfseqlem4a  9362  pwfseqlem4  9363  reclem2pr  9749  bnj1121  30307  bnj1189  30331  finminlem  31482  amosym1  31595  bj-ssbft  31831  bj-19.23bit  31868  bj-nexrt  31869  bj-19.9htbi  31881  bj-sbsb  32012  bj-nfdiOLD  32019  bj-xnex  32245  bj-finsumval0  32324  isbasisrelowllem1  32379  isbasisrelowllem2  32380  wl-exeq  32500  ax12indn  33246  gneispace  37452  pm11.58  37612  axc11next  37629  iotavalsb  37656  vk15.4j  37755  onfrALTlem1  37784  onfrALTlem1VD  38148  vk15.4jVD  38172  suprnmpt  38350  ssfiunibd  38464  ovncvrrp  39454  19.8ad  42257
  Copyright terms: Public domain W3C validator