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 1988
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 1845 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 1990. (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 1984 . . 3 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 ax6ev 1840 . . 3 𝑥 𝑥 = 𝑦
3 exim 1739 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥𝜑))
41, 2, 3syl6mpi 64 . 2 (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
5 ax6evr 1892 . 2 𝑦 𝑥 = 𝑦
64, 5exlimiiv 1812 1 (𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-12 1983
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  sp  1990  19.2g  1999  19.23bi  2002  nexr  2003  19.9t  2021  qexmid  2108  sbequ1  2129  ax6e  2141  exdistrf  2225  equvini  2238  2ax6e  2342  euor2  2406  2moex  2435  2euex  2436  2moswap  2439  2mo  2443  rspe  2890  ceqex  3207  mo2icl  3256  intab  4340  eusv2nf  4689  copsexg  4780  dmcosseq  5199  dminss  5356  imainss  5357  relssdmrn  5463  oprabid  6458  hta  8523  domtriomlem  9027  axextnd  9172  axrepnd  9175  axunndlem1  9176  axunnd  9177  axpowndlem2  9179  axpownd  9182  axregndlem1  9183  axregnd  9185  axacndlem1  9188  axacndlem2  9189  axacndlem3  9190  axacndlem4  9191  axacndlem5  9192  axacnd  9193  fpwwe  9227  pwfseqlem4a  9242  pwfseqlem4  9243  reclem2pr  9629  bnj1121  30156  bnj1189  30180  finminlem  31321  amosym1  31433  bj-ssbft  31669  bj-19.23bit  31706  bj-nexrt  31707  bj-19.9htbi  31719  bj-sbsb  31857  bj-nfdiOLD  31864  bj-xnex  32080  bj-finsumval0  32159  isbasisrelowllem1  32214  isbasisrelowllem2  32215  wl-nfr  32337  wl-19.9t  32344  wl-exeq  32393  ax12indn  33140  gneispace  37353  pm11.58  37513  axc11next  37530  iotavalsb  37557  vk15.4j  37656  onfrALTlem1  37685  onfrALTlem1VD  38049  vk15.4jVD  38073  suprnmpt  38252  ssfiunibd  38366  ovncvrrp  39365  19.8ad  42327
  Copyright terms: Public domain W3C validator