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 2170
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 1978 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2172. (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 2168 . . 3 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 alequexv 1998 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) → ∃𝑥𝜑)
31, 2syl6 35 . 2 (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
4 ax6evr 2013 . 2 𝑦 𝑥 = 𝑦
53, 4exlimiiv 1923 1 (𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  19.8ad  2171  sp  2172  19.2g  2177  19.23bi  2180  nexr  2181  qexmid  2182  nf5r  2183  nf5rOLD  2184  19.9t  2194  ax6e  2392  exdistrf  2461  equvini  2469  equviniOLD  2470  2ax6eOLD  2487  sb1OLD  2500  sbequ1OLD  2513  sbequ1ALT  2572  euor2  2690  2moexv  2705  2moswapv  2707  2euexv  2709  2moex  2718  2euex  2719  2moswap  2722  2mo  2726  rspe  3301  ceqex  3642  mo2icl  3702  intab  4897  eusv2nf  5286  copsexgw  5372  copsexg  5373  dmcosseq  5837  dminss  6003  imainss  6004  relssdmrn  6114  oprabidw  7176  oprabid  7177  hta  9314  axextnd  10001  axpowndlem2  10008  axregndlem1  10012  axregnd  10014  fpwwe  10056  reclem2pr  10458  bnj1121  32154  frrlem8  33027  frrlem10  33029  finminlem  33563  amosym1  33671  bj-19.23bit  33922  bj-nexrt  33923  bj-19.9htbi  33934  bj-sbsb  34057  bj-finsumval0  34455  wl-exeq  34655  ax12indn  35959  pm11.58  40599  axc11next  40615  iotavalsb  40642  vk15.4j  40739  onfrALTlem1  40759  onfrALTlem1VD  41101  vk15.4jVD  41125  suprnmpt  41306  ssfiunibd  41452
  Copyright terms: Public domain W3C validator