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 2038
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 1881 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2040. (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 2034 . . 3 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2 ax6ev 1876 . . 3 𝑥 𝑥 = 𝑦
3 exim 1750 . . 3 (∀𝑥(𝑥 = 𝑦𝜑) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥𝜑))
41, 2, 3syl6mpi 64 . 2 (𝑥 = 𝑦 → (𝜑 → ∃𝑥𝜑))
5 ax6evr 1928 . 2 𝑦 𝑥 = 𝑦
64, 5exlimiiv 1845 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 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  sp  2040  19.2g  2045  19.23bi  2048  nexr  2049  qexmid  2050  nf5r  2051  19.9t  2058  sbequ1  2095  19.9tOLD  2191  ax6e  2237  exdistrf  2320  equvini  2333  2ax6e  2437  euor2  2501  2moex  2530  2euex  2531  2moswap  2534  2mo  2538  rspe  2985  ceqex  3302  mo2icl  3351  intab  4436  eusv2nf  4785  copsexg  4876  dmcosseq  5295  dminss  5452  imainss  5453  relssdmrn  5559  oprabid  6554  hta  8620  domtriomlem  9124  axextnd  9269  axrepnd  9272  axunndlem1  9273  axunnd  9274  axpowndlem2  9276  axpownd  9279  axregndlem1  9280  axregnd  9282  axacndlem1  9285  axacndlem2  9286  axacndlem3  9287  axacndlem4  9288  axacndlem5  9289  axacnd  9290  fpwwe  9324  pwfseqlem4a  9339  pwfseqlem4  9340  reclem2pr  9726  bnj1121  30113  bnj1189  30137  finminlem  31288  amosym1  31401  bj-ssbft  31637  bj-19.23bit  31674  bj-nexrt  31675  bj-19.9htbi  31687  bj-sbsb  31818  bj-nfdiOLD  31825  bj-xnex  32041  bj-finsumval0  32120  isbasisrelowllem1  32175  isbasisrelowllem2  32176  wl-exeq  32296  ax12indn  33042  gneispace  37248  pm11.58  37408  axc11next  37425  iotavalsb  37452  vk15.4j  37551  onfrALTlem1  37580  onfrALTlem1VD  37944  vk15.4jVD  37968  suprnmpt  38146  ssfiunibd  38260  ovncvrrp  39251  19.8ad  42213
  Copyright terms: Public domain W3C validator