Theorem exlimiv 1931

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

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

This inference, along with its many variants such as rexlimdv 3242, 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 3242. 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. ∃𝑥𝜑(𝑥) where 𝜑(𝑥) 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 1931 to arrive at (∃𝑥𝜑 → 𝜓). Finally, we separately prove ∃𝑥𝜑 and detach it with modus ponens ax-mp 5 to arrive at the final theorem 𝜓, see exlimiiv 1932. (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 1970 and ax-8 2113. (Revised by Wolf Lammen, 4-Dec-2017.)

Hypothesis

Ref	Expression
exlimiv.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
exlimiv	⊢ (∃𝑥𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem exlimiv

Step	Hyp	Ref	Expression
1		exlimiv.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	eximi 1836	. 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
3		ax5e 1913	. 2 ⊢ (∃𝑥𝜓 → 𝜓)
4	2, 3	syl 17	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911

This theorem depends on definitions:  df-bi 210  df-ex 1782

This theorem is referenced by:  exlimiiv  1932  exlimivv  1933  exsbim  2008  ax8  2117  ax9  2125  dfeumo  2595  mo3  2623  mo4  2625  moanimv  2681  euanv  2686  mopick  2687  gencl  3481  cgsexg  3484  gencbvex2  3498  vtoclg  3515  vtocleg  3529  eqvincg  3589  elrabi  3623  sbcex2  3781  eluni  4803  intab  4868  uniintsn  4875  disjiun  5017  trintss  5153  intex  5204  axpweq  5230  eunex  5256  eusvnf  5258  eusvnfb  5259  reusv2lem3  5266  unipw  5308  moabex  5316  nnullss  5319  exss  5320  sbcop1  5344  mosubopt  5365  opelopabsb  5382  relop  5685  dmopab2rex  5750  dmrnssfld  5806  dmsnopg  6037  unixp0  6102  elsnxp  6110  iotauni  6299  iota1  6301  iota4  6305  dffv2  6733  fveqdmss  6823  eldmrexrnb  6835  exfo  6848  funop  6888  funopdmsn  6889  funsndifnop  6890  csbriota  7108  eusvobj2  7128  fnoprabg  7254  limuni3  7547  tfindsg  7555  findsg  7590  elxp5  7610  f1oexbi  7615  ffoss  7629  fo1stres  7697  fo2ndres  7698  eloprabi  7743  frxp  7803  suppimacnv  7824  mpoxneldm  7861  mpoxopxnop0  7864  reldmtpos  7883  dftpos4  7894  wfrlem2  7938  wfrlem3  7939  wfrlem4  7941  wfrdmcl  7946  wfrlem12  7949  tfrlem9  8004  ecdmn0  8319  mapprc  8393  ixpprc  8466  ixpn0  8477  bren  8501  brdomg  8502  ener  8539  en0  8555  en1  8559  en1b  8560  2dom  8565  fiprc  8578  pwdom  8653  domssex  8662  ssenen  8675  php  8685  isinf  8715  findcard2s  8743  hartogslem1  8990  brwdom  9015  brwdomn0  9017  wdompwdom  9026  unxpwdom2  9036  ixpiunwdom  9038  infeq5  9084  omex  9090  epfrs  9157  rankwflemb  9206  bnd2  9306  oncard  9373  carduni  9394  pm54.43  9414  ween  9446  acnrcl  9453  acndom  9462  acndom2  9465  iunfictbso  9525  aceq3lem  9531  dfac4  9533  dfac5lem4  9537  dfac5lem5  9538  dfac5  9539  dfac2a  9540  dfac2b  9541  dfacacn  9552  dfac12r  9557  kmlem2  9562  kmlem16  9576  ackbij2  9654  cff  9659  cardcf  9663  cfeq0  9667  cfsuc  9668  cff1  9669  cfcoflem  9683  coftr  9684  infpssr  9719  fin4en1  9720  isfin4-2  9725  enfin2i  9732  fin23lem21  9750  fin23lem30  9753  fin23lem41  9763  enfin1ai  9795  fin1a2lem7  9817  domtriomlem  9853  axdc2lem  9859  axdc3lem2  9862  axdc4lem  9866  axcclem  9868  ac6s  9895  zorn2lem7  9913  ttukey2g  9927  axdc  9932  brdom3  9939  brdom5  9940  brdom4  9941  brdom7disj  9942  brdom6disj  9943  konigthlem  9979  pwcfsdom  9994  pwfseq  10075  tsk0  10174  gruina  10229  ltbtwnnq  10389  reclem2pr  10459  supsrlem  10522  supsr  10523  axpre-sup  10580  dedekindle  10793  nnunb  11881  ioorebas  12829  fzn0  12916  fzon0  13050  axdc4uzlem  13346  hasheqf1oi  13708  hash1snb  13776  hash1n0  13778  hashf1lem2  13810  hashle2pr  13831  hashge2el2difr  13835  hashge3el3dif  13840  fi1uzind  13851  brfi1indALT  13854  swrdcl  13998  pfxcl  14030  relexpindlem  14414  fclim  14902  climmo  14906  rlimdmo1  14966  cicsym  17066  cictr  17067  brssc  17076  sscpwex  17077  initoid  17257  termoid  17258  initoeu1  17263  initoeu2lem1  17266  initoeu2  17268  termoeu1  17270  opifismgm  17861  grpidval  17863  dfgrp3e  18191  subgint  18295  giclcl  18404  gicrcl  18405  gicsym  18406  gicen  18409  gicsubgen  18410  cntzssv  18450  symgvalstruct  18517  giccyg  19013  brric2  19493  ricgic  19494  subrgint  19550  lmiclcl  19835  lmicrcl  19836  lmicsym  19837  abvn0b  20068  lmiclbs  20526  lmisfree  20531  lmictra  20534  mpfrcl  20757  ply1frcl  20942  pf1rcl  20973  mat1scmat  21144  toprntopon  21530  topnex  21601  neitr  21785  cmpsub  22005  bwth  22015  iunconn  22033  2ndcsb  22054  unisngl  22132  elpt  22177  ptclsg  22220  hmphsym  22387  hmphen  22390  haushmphlem  22392  cmphmph  22393  connhmph  22394  reghmph  22398  nrmhmph  22399  hmphdis  22401  indishmph  22403  hmphen2  22404  ufldom  22567  alexsubALTlem2  22653  alexsubALT  22656  metustfbas  23164  iunmbl2  24161  ioorcl2  24176  ioorinv2  24179  opnmblALT  24207  plyssc  24797  aannenlem2  24925  mulog2sum  26121  istrkg2ld  26254  axcontlem4  26761  lfuhgr1v0e  27044  nbgr1vtx  27148  edgusgrnbfin  27163  cplgr1vlem  27219  cplgr1v  27220  fusgrn0degnn0  27289  g0wlk0  27441  wspthneq1eq2  27646  wlkswwlksf1o  27665  wwlksnndef  27691  wspthsnonn0vne  27703  eulerpath  28026  frgrwopreglem2  28098  friendship  28184  shintcli  29112  strlem1  30033  rexunirn  30263  iunrnmptss  30329  cnvoprabOLD  30482  lsmsnorb  30999  mxidlnzrb  31052  prsdm  31267  prsrn  31268  0elsiga  31483  sigaclcu  31486  issgon  31492  insiga  31506  omssubaddlem  31667  omssubadd  31668  bnj521  32117  bnj906  32312  bnj938  32319  bnj1018g  32345  bnj1018  32346  bnj1020  32347  bnj1125  32374  bnj1145  32375  funen1cnv  32467  lfuhgr3  32479  loop1cycl  32497  satfrnmapom  32730  satf0op  32737  sat1el2xp  32739  dmopab3rexdif  32765  mppspstlem  32931  frrlem2  33237  frrlem3  33238  frrlem4  33239  frrlem8  33243  sslttr  33381  txpss3v  33452  pprodss4v  33458  elsingles  33492  fnimage  33503  funpartlem  33516  funpartfun  33517  dfrdg4  33525  colinearex  33634  bj-cleljusti  34126  axc11n11r  34130  bj-exlimvmpi  34351  bj-snglex  34409  bj-bm1.3ii  34481  bj-restpw  34507  mptsnunlem  34755  ctbssinf  34823  pibt2  34834  wl-moteq  34919  wl-sbcom2d  34962  wl-mo3t  34977  ptrecube  35057  mblfinlem3  35096  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  indexdom  35172  xrnss3v  35784  prtlem16  36165  sbccomieg  39734  setindtr  39965  setindtrs  39966  dfac11  40006  lnmlmic  40032  gicabl  40043  isnumbasgrplem1  40045  iscard4  40241  rtrclex  40317  clcnvlem  40323  brtrclfv2  40428  snhesn  40487  frege55b  40598  frege55c  40619  grucollcld  40968  grumnudlem  40993  iotain  41121  iotavalb  41134  sbiota1  41138  iunconnlem2  41641  fnchoice  41658  stoweidlem59  42701  vitali2  43333  nsssmfmbf  43412  funop1  43839  sbcpr  44038  opmpoismgm  44427  nzerooringczr  44696  setrec1lem3  45219  elsetrecs  45229  elpglem1  45240