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 2054
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 1897 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2056. (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 2050 . . 3 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 ax6ev 1892 . . 3 𝑥 𝑥 = 𝑦
3 exim 1758 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥𝜑))
41, 2, 3syl6mpi 67 . 2 (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
5 ax6evr 1944 . 2 𝑦 𝑥 = 𝑦
64, 5exlimiiv 1861 1 (𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1478  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-12 2049
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  sp  2056  19.2g  2061  19.23bi  2064  nexr  2065  qexmid  2066  nf5r  2067  19.9t  2074  sbequ1  2112  19.9tOLD  2208  ax6e  2254  exdistrf  2337  equvini  2350  2ax6e  2454  euor2  2518  2moex  2547  2euex  2548  2moswap  2551  2mo  2555  rspe  3002  ceqex  3321  mo2icl  3372  intab  4477  eusv2nf  4829  copsexg  4921  dmcosseq  5351  dminss  5510  imainss  5511  relssdmrn  5618  oprabid  6632  hta  8705  domtriomlem  9209  axextnd  9358  axrepnd  9361  axunndlem1  9362  axunnd  9363  axpowndlem2  9365  axpownd  9368  axregndlem1  9369  axregnd  9371  axacndlem1  9374  axacndlem2  9375  axacndlem3  9376  axacndlem4  9377  axacndlem5  9378  axacnd  9379  fpwwe  9413  pwfseqlem4a  9428  pwfseqlem4  9429  reclem2pr  9815  bnj1121  30753  bnj1189  30777  finminlem  31927  amosym1  32040  bj-ssbft  32257  bj-19.23bit  32296  bj-nexrt  32297  bj-19.9htbi  32309  bj-sbsb  32440  bj-nfdiOLD  32447  bj-xnex  32674  bj-finsumval0  32753  isbasisrelowllem1  32808  isbasisrelowllem2  32809  wl-exeq  32929  ax12indn  33675  gneispace  37881  pm11.58  38039  axc11next  38056  iotavalsb  38083  vk15.4j  38183  onfrALTlem1  38212  onfrALTlem1VD  38576  vk15.4jVD  38600  suprnmpt  38796  ssfiunibd  38955  ovncvrrp  40053  19.8ad  41706
  Copyright terms: Public domain W3C validator