MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.8a Structured version   Visualization version   Unicode version

Theorem 19.8a 1946
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 1822 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 1948. (Revised by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 8-Dec-2019.)
Assertion
Ref Expression
19.8a  |-  ( ph  ->  E. x ph )

Proof of Theorem 19.8a
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 ax12v 1945 . . . 4  |-  ( x  =  y  ->  ( ph  ->  A. x ( x  =  y  ->  ph )
) )
2 ax6ev 1818 . . . 4  |-  E. x  x  =  y
3 exim 1717 . . . 4  |-  ( A. x ( x  =  y  ->  ph )  -> 
( E. x  x  =  y  ->  E. x ph ) )
41, 2, 3syl6mpi 64 . . 3  |-  ( x  =  y  ->  ( ph  ->  E. x ph )
)
54equcoms 1875 . 2  |-  ( y  =  x  ->  ( ph  ->  E. x ph )
)
6 ax6ev 1818 . 2  |-  E. y 
y  =  x
75, 6exlimiiv 1788 1  |-  ( ph  ->  E. x ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1453   E.wex 1674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-12 1944
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675
This theorem is referenced by:  sp  1948  19.2g  1957  19.23bi  1960  nexr  1961  19.9t  1980  19.9tOLD  1983  qexmid  2068  sbequ1  2093  ax6e  2105  exdistrf  2178  equvini  2190  2ax6e  2290  euor2  2354  2moex  2383  2euex  2384  2moswap  2387  2mo  2391  rspe  2857  rsp2eOLD  2859  ceqex  3181  mo2icl  3229  intab  4279  eusv2nf  4618  copsexg  4704  dmcosseq  5118  dminss  5272  imainss  5273  relssdmrn  5379  oprabid  6347  hta  8399  domtriomlem  8903  axextnd  9047  axrepnd  9050  axunndlem1  9051  axunnd  9052  axpowndlem2  9054  axpownd  9057  axregndlem1  9058  axregnd  9060  axacndlem1  9063  axacndlem2  9064  axacndlem3  9065  axacndlem4  9066  axacndlem5  9067  axacnd  9068  fpwwe  9102  pwfseqlem4a  9117  pwfseqlem4  9118  reclem2pr  9504  bnj1121  29844  bnj1189  29868  finminlem  31024  amosym1  31136  bj-ssbft  31301  bj-19.23bit  31330  bj-nexrt  31331  bj-19.9htbi  31343  bj-nfdiOLD  31490  bj-finsumval0  31748  isbasisrelowllem1  31804  isbasisrelowllem2  31805  wl-exeq  31913  ax12indn  32560  pm11.58  36785  axc11next  36802  iotavalsb  36829  vk15.4j  36930  onfrALTlem1  36959  onfrALTlem1VD  37328  vk15.4jVD  37352  suprnmpt  37493  ssfiunibd  37602  ovncvrrp  38493  19.8ad  40806
  Copyright terms: Public domain W3C validator