Theorem exlimiv 1730

Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 1918.

See exlimi 1920 for a more general version requiring more axioms.

This inference, along with its many variants such as rexlimdv 2872, is used to implement a metatheorem called "Rule C" that is given in many logic textbooks. See, for example, Rule C in [Mendelson] p. 81, Rule C in [Margaris] p. 40, or Rule C in Hirst and Hirst's A Primer for Logic and Proof p. 59 (PDF p. 65) at http://www.appstate.edu/~hirstjl/primer/hirst.pdf. In informal proofs, the statement "Let C be an element such that..." almost always means an implicit application of Rule C.

In essence, Rule C states that if we can prove that some element x exists satisfying a wff, i.e. E. x ph ( x ) where ph ( x ) has x free, then we can use ph ( C ) as a hypothesis for the proof where C is a new (fictitious) constant not appearing previously in the proof, nor in any axioms used, nor in the theorem to be proved. The purpose of Rule C is to get rid of the existential quantifier.

We cannot do this in Metamath directly. Instead, we use the original ph (containing x) as an antecedent for the main part of the proof. We eventually arrive at ( ph -> ps ) where ps is the theorem to be proved and does not contain x. Then we apply exlimiv 1730 to arrive at ( E. x ph -> ps ). Finally, we separately prove E. x ph and detach it with modus ponens ax-mp 5 to arrive at the final theorem ps. (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 1755 and ax-8 1828. (Revised by Wolf Lammen, 4-Dec-2017.)

Hypothesis

Ref	Expression
exlimiv.1	|- ( ph -> ps )

Assertion

Ref	Expression
exlimiv	|- ( E. x ph -> ps )

Distinct variable group:   ps, x

Allowed substitution hint:   ph( x)

Proof of Theorem exlimiv

Step	Hyp	Ref	Expression
1		exlimiv.1	. . 3 |- ( ph -> ps )
2	1	eximi 1664	. 2 |- ( E. x ph -> E. x ps )
3		ax5e 1714	. 2 |- ( E. x ps -> ps )
4	2, 3	syl 16	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   E.wex 1620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712

This theorem depends on definitions:  df-bi 185  df-ex 1621

This theorem is referenced by:  exlimivv  1731  equvin  1812  ax12v  1863  ax12vOLD  1864  19.8a  1865  19.8aOLD  1866  ax6e  2009  axc11n  2055  axc11nOLD  2056  sbcom2  2193  euex  2244  mo3  2258  mo3OLD  2259  mopick  2287  mopickOLD  2288  axext3  2362  gencl  3064  cgsexg  3067  gencbvex2  3079  vtocleg  3105  eqvinc  3151  elrabi  3179  sbcex2  3303  eluni  4166  intab  4230  uniintsn  4237  disjiun  4358  trint0  4477  bm1.3ii  4491  intex  4521  axpweq  4542  eunex  4558  eusvnf  4560  eusvnfb  4561  reusv2lem3  4568  unipw  4612  moabex  4621  nnullss  4624  exss  4625  mosubopt  4659  opelopabsb  4671  relop  5066  dmrnssfld  5174  dmsnopg  5387  unixp0  5450  iotauni  5472  iota1  5474  iota4  5478  dffv2  5847  fveqdmss  5928  eldmrexrnb  5940  exfo  5951  csbriota  6170  eusvobj2  6189  fnoprabg  6302  limuni3  6586  tfindsg  6594  findsg  6626  elxp5  6644  f1oexbi  6649  ffoss  6660  fo1stres  6723  fo2ndres  6724  eloprabi  6761  frxp  6809  suppimacnv  6828  mpt2xopxnop0  6861  reldmtpos  6881  dftpos4  6892  tfrlem9  6972  ecdmn0  7272  mapprc  7342  ixpprc  7409  ixpn0  7420  bren  7444  brdomg  7445  ener  7481  en0  7497  en1  7501  en1b  7502  2dom  7507  fiprc  7516  pwdom  7588  domssex  7597  ssenen  7610  php  7620  isinf  7649  findcard2s  7676  hartogslem1  7882  brwdom  7908  brwdomn0  7910  wdompwdom  7919  unxpwdom2  7929  ixpiunwdom  7932  inf3  7966  infeq5  7968  omex  7974  epfrs  8075  rankwflemb  8124  bnd2  8224  oncard  8254  carduni  8275  pm54.43  8294  ween  8329  acnrcl  8336  acndom  8345  acndom2  8348  iunfictbso  8408  aceq3lem  8414  dfac4  8416  dfac5lem4  8420  dfac5lem5  8421  dfac5  8422  dfac2a  8423  dfac2  8424  dfacacn  8434  dfac12r  8439  kmlem2  8444  kmlem16  8458  ackbij2  8536  cff  8541  cardcf  8545  cfeq0  8549  cfsuc  8550  cff1  8551  cfcoflem  8565  coftr  8566  infpssr  8601  fin4en1  8602  isfin4-2  8607  enfin2i  8614  fin23lem21  8632  fin23lem30  8635  fin23lem41  8645  enfin1ai  8677  fin1a2lem7  8699  axcc2lem  8729  domtriomlem  8735  dcomex  8740  axdc2lem  8741  axdc3lem2  8744  axdc4lem  8748  axcclem  8750  ac6s  8777  zorn2lem7  8795  ttukey2g  8809  axdclem2  8813  axdc  8814  brdom3  8819  brdom5  8820  brdom4  8821  brdom7disj  8822  brdom6disj  8823  konigthlem  8856  pwcfsdom  8871  pwfseq  8953  tsk0  9052  gruina  9107  grothpw  9115  grothpwex  9116  grothomex  9118  grothac  9119  ltbtwnnq  9267  reclem2pr  9337  supsrlem  9399  supsr  9400  axpre-sup  9457  dedekindle  9656  nnunb  10708  ioorebas  11547  fzn0  11621  fzon0  11739  axdc4uzlem  11995  hasheqf1oi  12326  hash1snb  12383  hashf1lem2  12409  hashge3el3dif  12428  brfi1uzind  12436  swrdcl  12555  relexpindlem  12898  fclim  13378  climmo  13382  rlimdmo1  13442  cnso  13982  xpsfrnel2  14972  cicsym  15210  cictr  15211  brssc  15220  sscpwex  15221  initoid  15401  termoid  15402  initoeu1  15407  initoeu2lem1  15410  initoeu2  15412  termoeu1  15414  opifismgm  16002  grpidval  16004  subgint  16342  giclcl  16437  gicrcl  16438  gicsym  16439  gicen  16442  gicsubgen  16443  cntzssv  16483  giccyg  17019  brric2  17507  ricgic  17508  subrgint  17564  lmiclcl  17829  lmicrcl  17830  lmicsym  17831  abvn0b  18064  mpfrcl  18300  ply1frcl  18468  pf1rcl  18498  lmiclbs  18957  lmisfree  18962  lmictra  18965  mat1scmat  19126  neitr  19767  cmpsub  19986  bwth  19996  iuncon  20014  2ndcsb  20035  unisngl  20113  elpt  20158  ptclsg  20201  hmphsym  20368  hmphen  20371  haushmphlem  20373  cmphmph  20374  conhmph  20375  reghmph  20379  nrmhmph  20380  hmphdis  20382  indishmph  20384  hmphen2  20385  ufldom  20548  alexsubALTlem2  20633  alexsubALT  20636  metustfbasOLD  21153  metustfbas  21154  iunmbl2  22052  ioorcl2  22066  ioorinv2  22069  opnmblALT  22097  plyssc  22682  aannenlem2  22810  aannenlem3  22811  mulog2sum  23839  istrkg2ld  23975  axcontlem4  24391  usgraedg4  24508  edgusgranbfin  24571  uvtx01vtx  24613  3v3e3cycl2  24785  wlknwwlknsur  24833  wlkiswwlksur  24840  wwlknndef  24858  wlk0  24882  clwwlknndef  24894  2spontn0vne  25008  rusgrasn  25066  eupath  25102  vdfrgra0  25143  usgn0fidegnn0  25150  frgrawopreglem2  25166  friendship  25243  shintcli  26364  strlem1  27285  eqvincg  27491  rexunirn  27507  ctex  27680  cnvoprab  27696  prsdm  28050  prsrn  28051  0elsiga  28263  sigaclcu  28266  issgon  28272  insiga  28286  omssubaddlem  28426  omssubadd  28427  mppspstlem  29120  wfrlem2  29509  wfrlem3  29510  wfrlem4  29511  wfrlem9  29516  wfrlem12  29519  frrlem2  29553  frrlem3  29554  frrlem4  29555  frrlem5e  29560  frrlem11  29564  txpss3v  29681  pprodss4v  29687  elsingles  29721  fnimage  29732  funpartlem  29745  funpartfun  29746  dfrdg4  29753  colinearex  29863  wl-sbcom2d  30176  wl-mo3t  30186  mblfinlem3  30218  ovoliunnfl  30221  voliunnfl  30223  volsupnfl  30224  indexdom  30391  prtlem16  30776  sbccomieg  30892  setindtr  31132  setindtrs  31133  dfac11  31174  lnmlmic  31200  gicabl  31215  isnumbasgrplem1  31218  iotain  31492  iotavalb  31505  sbiota1  31509  fnchoice  31571  stoweidlem59  32007  pfxcl  32561  opmpt2ismgm  32813  nzerooringczr  33080  iunconlem2  34082  bnj521  34139  bnj906  34335  bnj938  34342  bnj1018  34367  bnj1020  34368  bnj1125  34395  bnj1145  34396  bj-equsexvv  34660  bj-axc11nv  34663  bj-eunex  34732  bj-snglex  34879  brtrclfv2  38258  snhesn  38281  frege55b  38396  frege55c  38417