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 2050
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 1893 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2051. (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 2046 . . 3 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 ax6ev 1888 . . 3 𝑥 𝑥 = 𝑦
3 exim 1759 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥𝜑))
41, 2, 3syl6mpi 67 . 2 (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
5 ax6evr 1940 . 2 𝑦 𝑥 = 𝑦
64, 5exlimiiv 1857 1 (𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1479  wex 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-12 2045
This theorem depends on definitions:  df-bi 197  df-ex 1703
This theorem is referenced by:  sp  2051  19.2g  2056  19.23bi  2059  nexr  2060  qexmid  2061  nf5r  2062  19.9t  2069  sbequ1  2108  19.9tOLD  2202  ax6e  2248  exdistrf  2331  equvini  2344  2ax6e  2448  euor2  2512  2moex  2541  2euex  2542  2moswap  2545  2mo  2549  rspe  3000  ceqex  3327  mo2icl  3379  intab  4498  eusv2nf  4855  copsexg  4946  dmcosseq  5376  dminss  5535  imainss  5536  relssdmrn  5644  oprabid  6662  hta  8745  domtriomlem  9249  axextnd  9398  axrepnd  9401  axunndlem1  9402  axunnd  9403  axpowndlem2  9405  axpownd  9408  axregndlem1  9409  axregnd  9411  axacndlem1  9414  axacndlem2  9415  axacndlem3  9416  axacndlem4  9417  axacndlem5  9418  axacnd  9419  fpwwe  9453  pwfseqlem4a  9468  pwfseqlem4  9469  reclem2pr  9855  bnj1121  31027  bnj1189  31051  finminlem  32287  amosym1  32400  bj-ssbft  32617  bj-19.23bit  32656  bj-nexrt  32657  bj-19.9htbi  32669  bj-sbsb  32799  bj-finsumval0  33118  isbasisrelowllem1  33174  isbasisrelowllem2  33175  wl-exeq  33292  ax12indn  34047  gneispace  38252  pm11.58  38410  axc11next  38427  iotavalsb  38454  vk15.4j  38554  onfrALTlem1  38583  onfrALTlem1VD  38946  vk15.4jVD  38970  suprnmpt  39171  ssfiunibd  39336  ovncvrrp  40541  19.8ad  42223
  Copyright terms: Public domain W3C validator