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 2225
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 2085 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2226. (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 2223 . . 3 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 ax6ev 2079 . . 3 𝑥 𝑥 = 𝑦
3 exim 1934 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥𝜑))
41, 2, 3syl6mpi 67 . 2 (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
5 ax6evr 2121 . 2 𝑦 𝑥 = 𝑦
64, 5exlimiiv 2032 1 (𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1656  wex 1880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-12 2222
This theorem depends on definitions:  df-bi 199  df-ex 1881
This theorem is referenced by:  sp  2226  19.2g  2231  19.23bi  2234  nexr  2235  qexmid  2236  nf5r  2237  19.9t  2248  sbequ1  2287  ax6e  2403  exdistrf  2467  equvini  2475  2ax6e  2583  euor2  2700  2moex  2722  2euex  2723  2moswap  2726  2mo  2730  rspe  3210  ceqex  3550  mo2icl  3609  intab  4726  eusv2nf  5094  copsexg  5175  dmcosseq  5619  dminss  5787  imainss  5788  relssdmrn  5896  oprabid  6935  hta  9036  domtriomlem  9578  axextnd  9727  axrepnd  9730  axunndlem1  9731  axunnd  9732  axpowndlem2  9734  axpownd  9737  axregndlem1  9738  axregnd  9740  axacndlem1  9743  axacndlem2  9744  axacndlem3  9745  axacndlem4  9746  axacndlem5  9747  axacnd  9748  fpwwe  9782  pwfseqlem4a  9797  pwfseqlem4  9798  reclem2pr  10184  bnj1121  31598  bnj1189  31622  frrlem11  32330  finminlem  32850  amosym1  32957  bj-ssbft  33177  bj-19.23bit  33215  bj-nexrt  33216  bj-19.9htbi  33227  bj-sbsb  33347  bj-finsumval0  33698  isbasisrelowllem1  33747  isbasisrelowllem2  33748  wl-exeq  33864  ax12indn  35017  gneispace  39271  pm11.58  39429  axc11next  39445  iotavalsb  39472  vk15.4j  39571  onfrALTlem1  39591  onfrALTlem1VD  39943  vk15.4jVD  39967  suprnmpt  40163  ssfiunibd  40320  ovncvrrp  41571  19.8ad  43355
  Copyright terms: Public domain W3C validator