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 2176
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 1983 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2178. (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 2174 . . 3 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 alequexv 2003 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) → ∃𝑥𝜑)
31, 2syl6 35 . 2 (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
4 ax6evr 2018 . 2 𝑦 𝑥 = 𝑦
53, 4exlimiiv 1928 1 (𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1531  wex 1776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2173
This theorem depends on definitions:  df-bi 209  df-ex 1777
This theorem is referenced by:  19.8ad  2177  sp  2178  19.2g  2183  19.23bi  2186  nexr  2187  qexmid  2188  nf5r  2189  nf5rOLD  2190  19.9t  2200  ax6e  2397  exdistrf  2465  equvini  2473  equviniOLD  2474  2ax6eOLD  2491  sb1OLD  2503  sbequ1OLD  2516  sbequ1ALT  2575  euor2  2693  2moexv  2708  2moswapv  2710  2euexv  2712  2moex  2721  2euex  2722  2moswap  2725  2mo  2729  rspe  3304  ceqex  3644  mo2icl  3704  intab  4905  eusv2nf  5295  copsexgw  5380  copsexg  5381  dmcosseq  5843  dminss  6009  imainss  6010  relssdmrn  6120  oprabidw  7186  oprabid  7187  hta  9325  axextnd  10012  axpowndlem2  10019  axregndlem1  10023  axregnd  10025  fpwwe  10067  reclem2pr  10469  bnj1121  32257  frrlem8  33130  frrlem10  33132  finminlem  33666  amosym1  33774  bj-19.23bit  34025  bj-nexrt  34026  bj-19.9htbi  34037  bj-sbsb  34160  bj-finsumval0  34566  wl-exeq  34773  ax12indn  36078  pm11.58  40722  axc11next  40738  iotavalsb  40765  vk15.4j  40862  onfrALTlem1  40882  onfrALTlem1VD  41224  vk15.4jVD  41248  suprnmpt  41430  ssfiunibd  41576
  Copyright terms: Public domain W3C validator