Theorem exlimiv 1722

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

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

This inference, along with its many variants such as rexlimdv 2947, 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 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 exists satisfying a wff, i.e. E.x(x) where (x) has free, then we can use () as a hypothesis for the proof where 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 (containing ) as an antecedent for the main part of the proof. We eventually arrive at where is the theorem to be proved and does not contain . Then we apply exlimiv 1722 to arrive at . Finally, we separately prove and detach it with modus ponens ax-mp 5 to arrive at the final theorem . (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 1747 and ax-8 1820. (Revised by Wolf Lammen, 4-Dec-2017.)

Hypothesis

Ref	Expression
exlimiv.1

Assertion

Ref	Expression
exlimiv

Distinct variable group:   ,

Proof of Theorem exlimiv

Step	Hyp	Ref	Expression
1		exlimiv.1	. . 3
2	1	eximi 1656	. 2
3		ax5e 1706	. 2
4	2, 3	syl 16	1

Syntax hints:  ->wi 4  E.wex 1612

This theorem is referenced by:  exlimivv  1723  equvin  1804  ax12v  1855  ax12vOLD  1856  19.8a  1857  19.8aOLD  1858  ax6e  2002  axc11n  2049  axc11nOLD  2050  equvinOLD  2090  sbcom2  2189  euex  2308  mo3  2323  mo3OLD  2324  mopick  2356  mopickOLD  2357  axext3  2437  gencl  3139  cgsexg  3142  gencbvex2  3154  vtocleg  3180  eqvinc  3226  elrabi  3254  sbcex2  3381  eluni  4252  intab  4317  uniintsn  4324  disjiun  4442  trint0  4562  bm1.3ii  4576  intex  4608  axpweq  4629  eunex  4645  eusvnf  4647  eusvnfb  4648  reusv2lem3  4655  unipw  4702  moabex  4711  nnullss  4714  exss  4715  mosubopt  4750  opelopabsb  4762  relop  5158  dmrnssfld  5266  dmsnopg  5484  unixp0  5546  iotauni  5568  iota1  5570  iota4  5574  dffv2  5946  fveqdmss  6026  eldmrexrnb  6038  exfo  6049  csbriota  6269  eusvobj2  6289  fnoprabg  6403  limuni3  6687  tfindsg  6695  findsg  6727  elxp5  6745  f1oexbi  6750  ffoss  6761  fo1stres  6824  fo2ndres  6825  eloprabi  6862  frxp  6910  suppimacnv  6929  mpt2xopxnop0  6962  reldmtpos  6982  dftpos4  6993  tfrlem9  7073  ecdmn0  7373  mapprc  7443  ixpprc  7510  ixpn0  7521  bren  7545  brdomg  7546  ener  7582  en0  7598  en1  7602  en1b  7603  2dom  7608  fiprc  7617  pwdom  7689  domssex  7698  ssenen  7711  php  7721  isinf  7753  findcard2s  7781  hartogslem1  7988  brwdom  8014  brwdomn0  8016  wdompwdom  8025  unxpwdom2  8035  ixpiunwdom  8038  inf3  8073  infeq5  8075  omex  8081  epfrs  8183  rankwflemb  8232  bnd2  8332  oncard  8362  carduni  8383  pm54.43  8402  ween  8437  acnrcl  8444  acndom  8453  acndom2  8456  iunfictbso  8516  aceq3lem  8522  dfac4  8524  dfac5lem4  8528  dfac5lem5  8529  dfac5  8530  dfac2a  8531  dfac2  8532  dfacacn  8542  dfac12r  8547  kmlem2  8552  kmlem16  8566  ackbij2  8644  cff  8649  cardcf  8653  cfeq0  8657  cfsuc  8658  cff1  8659  cfcoflem  8673  coftr  8674  infpssr  8709  fin4en1  8710  isfin4-2  8715  enfin2i  8722  fin23lem21  8740  fin23lem30  8743  fin23lem41  8753  enfin1ai  8785  fin1a2lem7  8807  axcc2lem  8837  domtriomlem  8843  dcomex  8848  axdc2lem  8849  axdc3lem2  8852  axdc4lem  8856  axcclem  8858  ac6s  8885  zorn2lem7  8903  ttukey2g  8917  axdclem2  8921  axdc  8922  brdom3  8927  brdom5  8928  brdom4  8929  brdom7disj  8930  brdom6disj  8931  konigthlem  8964  pwcfsdom  8979  pwfseq  9063  tsk0  9162  gruina  9217  grothpw  9225  grothpwex  9226  grothomex  9228  grothac  9229  ltbtwnnq  9377  reclem2pr  9447  supsrlem  9509  supsr  9510  axpre-sup  9567  dedekindle  9766  nnunb  10816  ioorebas  11655  fzn0  11729  fzon0  11845  axdc4uzlem  12092  hasheqf1oi  12424  hash1snb  12479  hashf1lem2  12505  hashge3el3dif  12524  brfi1uzind  12532  swrdcl  12646  fclim  13376  climmo  13380  rlimdmo1  13440  cnso  13980  xpsfrnel2  14962  brssc  15183  sscpwex  15184  opifismgm  15885  grpidval  15887  subgint  16225  giclcl  16320  gicrcl  16321  gicsym  16322  gicen  16325  gicsubgen  16326  cntzssv  16366  giccyg  16902  brric2  17394  ricgic  17395  subrgint  17451  lmiclcl  17716  lmicrcl  17717  lmicsym  17718  abvn0b  17951  mpfrcl  18187  ply1frcl  18355  pf1rcl  18385  lmiclbs  18872  lmisfree  18877  lmictra  18880  mat1scmat  19041  neitr  19681  cmpsub  19900  bwth  19910  bwthOLD  19911  iuncon  19929  2ndcsb  19950  unisngl  20028  elpt  20073  ptclsg  20116  hmphsym  20283  hmphen  20286  haushmphlem  20288  cmphmph  20289  conhmph  20290  reghmph  20294  nrmhmph  20295  hmphdis  20297  indishmph  20299  hmphen2  20300  ufldom  20463  alexsubALTlem2  20548  alexsubALT  20551  metustfbasOLD  21068  metustfbas  21069  iunmbl2  21967  ioorcl2  21981  ioorinv2  21984  opnmblALT  22012  plyssc  22597  aannenlem2  22725  aannenlem3  22726  mulog2sum  23722  istrkg2ld  23858  axcontlem4  24270  usgraedg4  24387  edgusgranbfin  24450  uvtx01vtx  24492  3v3e3cycl2  24664  wlknwwlknsur  24712  wlkiswwlksur  24719  wwlknndef  24737  wlk0  24761  clwwlknndef  24773  2spontn0vne  24887  rusgrasn  24945  eupath  24981  vdfrgra0  25022  usgn0fidegnn0  25029  frgrawopreglem2  25045  friendship  25122  shintcli  26247  strlem1  27169  eqvincg  27374  rexunirn  27390  ctex  27531  cnvoprab  27546  prsdm  27896  prsrn  27897  0elsiga  28114  sigaclcu  28117  issgon  28123  insiga  28137  mppspstlem  28931  relexpindlem  29062  wfrlem2  29344  wfrlem3  29345  wfrlem4  29346  wfrlem9  29351  wfrlem12  29354  frrlem2  29388  frrlem3  29389  frrlem4  29390  frrlem5e  29395  frrlem11  29399  txpss3v  29528  pprodss4v  29534  elsingles  29568  fnimage  29579  funpartlem  29592  funpartfun  29593  dfrdg4  29600  colinearex  29710  wl-sbcom2d  30011  wl-mo3t  30021  mblfinlem3  30053  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  indexdom  30225  prtlem16  30610  sbccomieg  30726  setindtr  30966  setindtrs  30967  dfac11  31008  lnmlmic  31034  gicabl  31047  isnumbasgrplem1  31050  iotain  31324  iotavalb  31337  sbiota1  31341  fnchoice  31404  stoweidlem59  31841  opmpt2ismgm  32495  cicsym  32588  cictr  32589  initoid  32611  termoid  32612  initoeu1  32617  initoeu2lem1  32620  initoeu2  32622  termoeu1  32624  nzerooringczr  32880  iunconlem2  33735  bnj521  33792  bnj906  33988  bnj938  33995  bnj1018  34020  bnj1020  34021  bnj1125  34048  bnj1145  34049  bj-equsexvv  34313  bj-axc11nv  34316  bj-eunex  34385  bj-snglex  34531  snhesn  37809  frege55b  37924  frege55c  37945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704

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