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 2090
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 1952 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2091. (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 2088 . . 3 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 ax6ev 1947 . . 3 𝑥 𝑥 = 𝑦
3 exim 1801 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥𝜑))
41, 2, 3syl6mpi 67 . 2 (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
5 ax6evr 1988 . 2 𝑦 𝑥 = 𝑦
64, 5exlimiiv 1899 1 (𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521  wex 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-ex 1745
This theorem is referenced by:  sp  2091  19.2g  2096  19.23bi  2099  nexr  2100  qexmid  2101  nf5r  2102  19.9t  2109  sbequ1  2148  19.9tOLD  2240  ax6e  2286  exdistrf  2364  equvini  2374  2ax6e  2478  euor2  2543  2moex  2572  2euex  2573  2moswap  2576  2mo  2580  rspe  3032  ceqex  3364  mo2icl  3418  intab  4539  eusv2nf  4894  copsexg  4985  dmcosseq  5419  dminss  5582  imainss  5583  relssdmrn  5694  oprabid  6717  hta  8798  domtriomlem  9302  axextnd  9451  axrepnd  9454  axunndlem1  9455  axunnd  9456  axpowndlem2  9458  axpownd  9461  axregndlem1  9462  axregnd  9464  axacndlem1  9467  axacndlem2  9468  axacndlem3  9469  axacndlem4  9470  axacndlem5  9471  axacnd  9472  fpwwe  9506  pwfseqlem4a  9521  pwfseqlem4  9522  reclem2pr  9908  bnj1121  31179  bnj1189  31203  frrlem11  31917  finminlem  32437  amosym1  32550  bj-ssbft  32767  bj-19.23bit  32806  bj-nexrt  32807  bj-19.9htbi  32819  bj-sbsb  32949  bj-finsumval0  33277  isbasisrelowllem1  33333  isbasisrelowllem2  33334  wl-exeq  33451  ax12indn  34547  gneispace  38749  pm11.58  38907  axc11next  38924  iotavalsb  38951  vk15.4j  39051  onfrALTlem1  39080  onfrALTlem1VD  39440  vk15.4jVD  39464  suprnmpt  39669  ssfiunibd  39837  ovncvrrp  41099  19.8ad  42786
  Copyright terms: Public domain W3C validator