Theorem exlimiv 1936

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

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

This inference, along with its many variants such as rexlimdv 3192, 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 3192. 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 1936 to arrive at (∃𝑥𝜑 → 𝜓). Finally, we separately prove ∃𝑥𝜑 and detach it with modus ponens ax-mp 5 to arrive at the final theorem 𝜓, see exlimiiv 1937. (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 1974 and ax-8 2115. (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 1841	. 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
3		ax5e 1918	. 2 ⊢ (∃𝑥𝜓 → 𝜓)
4	2, 3	syl 17	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916

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

This theorem is referenced by:  exlimiiv  1937  exlimivv  1938  exsbim  2012  ax8  2119  ax9  2127  dfeumo  2537  mo3  2564  mo4  2566  moanimv  2622  euanv  2627  mopick  2628  clelab  2875  gencl  3436  cgsexg  3439  gencbvex2  3453  vtoclg  3470  vtocleg  3484  eqvincg  3542  elrabi  3579  elrabiOLD  3580  sbcex2  3741  eluni  4796  intab  4863  uniintsn  4872  disjiun  5014  trintss  5150  intex  5202  axpweq  5228  eunex  5254  eusvnf  5256  eusvnfb  5257  reusv2lem3  5264  unipw  5306  moabex  5314  nnullss  5317  exss  5318  sbcop1  5342  mosubopt  5364  opelopabsb  5382  relop  5687  dmopab2rex  5754  dmrnssfld  5807  dmsnopg  6039  unixp0  6109  elsnxp  6117  iotauni  6308  iota1  6310  iota4  6314  dffv2  6757  fveqdmss  6850  eldmrexrnb  6862  exfo  6875  funop  6915  funopdmsn  6916  funsndifnop  6917  csbriota  7137  eusvobj2  7157  fnoprabg  7283  limuni3  7580  tfindsg  7588  findsg  7623  elxp5  7647  f1oexbi  7652  ffoss  7665  fo1stres  7733  fo2ndres  7734  eloprabi  7779  frxp  7839  suppimacnv  7862  mpoxneldm  7900  mpoxopxnop0  7903  reldmtpos  7922  dftpos4  7933  wfrlem2  7977  wfrlem3  7978  wfrlem4  7980  wfrdmcl  7985  wfrlem12  7988  tfrlem9  8043  ecdmn0  8360  mapprc  8434  fsetprcnex  8465  ixpprc  8522  ixpn0  8533  bren  8557  brdomg  8558  ener  8595  en0  8611  en0OLD  8612  en1  8616  en1b  8617  2dom  8622  fiprc  8636  pwdom  8712  domssex  8721  ssenen  8734  php  8744  rexdif1en  8753  dif1en  8754  findcard2s  8757  pwfir  8767  ensymfib  8775  isinf  8803  hartogslem1  9072  brwdom  9097  brwdomn0  9099  wdompwdom  9108  unxpwdom2  9118  ixpiunwdom  9120  infeq5  9166  omex  9172  epfrs  9239  rankwflemb  9288  bnd2  9388  oncard  9455  carduni  9476  pm54.43  9496  ween  9528  acnrcl  9535  acndom  9544  acndom2  9547  iunfictbso  9607  aceq3lem  9613  dfac4  9615  dfac5lem4  9619  dfac5lem5  9620  dfac5  9621  dfac2a  9622  dfac2b  9623  dfacacn  9634  dfac12r  9639  kmlem2  9644  kmlem16  9658  ackbij2  9736  cff  9741  cardcf  9745  cfeq0  9749  cfsuc  9750  cff1  9751  cfcoflem  9765  coftr  9766  infpssr  9801  fin4en1  9802  isfin4-2  9807  enfin2i  9814  fin23lem21  9832  fin23lem30  9835  fin23lem41  9845  enfin1ai  9877  fin1a2lem7  9899  domtriomlem  9935  axdc2lem  9941  axdc3lem2  9944  axdc4lem  9948  axcclem  9950  ac6s  9977  zorn2lem7  9995  ttukey2g  10009  axdc  10014  brdom3  10021  brdom5  10022  brdom4  10023  brdom7disj  10024  brdom6disj  10025  konigthlem  10061  pwcfsdom  10076  pwfseq  10157  tsk0  10256  gruina  10311  ltbtwnnq  10471  reclem2pr  10541  supsrlem  10604  supsr  10605  axpre-sup  10662  dedekindle  10875  nnunb  11965  ioorebas  12918  fzn0  13005  fzon0  13139  axdc4uzlem  13435  hasheqf1oi  13797  hash1snb  13865  hash1n0  13867  hashf1lem2  13901  hashle2pr  13922  hashge2el2difr  13926  hashge3el3dif  13931  fi1uzind  13942  brfi1indALT  13945  swrdcl  14089  pfxcl  14121  relexpindlem  14505  fclim  14993  climmo  14997  rlimdmo1  15058  cicsym  17172  cictr  17173  brssc  17182  sscpwex  17183  initoid  17366  termoid  17367  initoeu1  17376  initoeu2lem1  17379  initoeu2  17381  termoeu1  17383  opifismgm  17978  grpidval  17980  dfgrp3e  18310  subgint  18414  giclcl  18523  gicrcl  18524  gicsym  18525  gicen  18528  gicsubgen  18529  cntzssv  18569  symgvalstruct  18636  giccyg  19132  brric2  19612  ricgic  19613  subrgint  19669  lmiclcl  19954  lmicrcl  19955  lmicsym  19956  abvn0b  20187  lmiclbs  20646  lmisfree  20651  lmictra  20654  mpfrcl  20892  ply1frcl  21081  pf1rcl  21112  mat1scmat  21283  toprntopon  21669  topnex  21740  neitr  21924  cmpsub  22144  bwth  22154  iunconn  22172  2ndcsb  22193  unisngl  22271  elpt  22316  ptclsg  22359  hmphsym  22526  hmphen  22529  haushmphlem  22531  cmphmph  22532  connhmph  22533  reghmph  22537  nrmhmph  22538  hmphdis  22540  indishmph  22542  hmphen2  22543  ufldom  22706  alexsubALTlem2  22792  alexsubALT  22795  metustfbas  23303  iunmbl2  24302  ioorcl2  24317  ioorinv2  24320  opnmblALT  24348  plyssc  24941  aannenlem2  25069  mulog2sum  26265  istrkg2ld  26398  axcontlem4  26905  lfuhgr1v0e  27188  nbgr1vtx  27292  edgusgrnbfin  27307  cplgr1vlem  27363  cplgr1v  27364  fusgrn0degnn0  27433  g0wlk0  27585  wspthneq1eq2  27790  wlkswwlksf1o  27809  wwlksnndef  27835  wspthsnonn0vne  27847  eulerpath  28170  frgrwopreglem2  28242  friendship  28328  shintcli  29256  strlem1  30177  rexunirn  30406  iunrnmptss  30471  cnvoprabOLD  30622  lsmsnorb  31143  mxidlnzrb  31208  prsdm  31428  prsrn  31429  0elsiga  31644  sigaclcu  31647  issgon  31653  insiga  31667  omssubaddlem  31828  omssubadd  31829  bnj521  32278  bnj906  32473  bnj938  32480  bnj1018g  32506  bnj1018  32507  bnj1020  32508  bnj1125  32535  bnj1145  32536  funen1cnv  32623  fineqvac  32629  lfuhgr3  32644  loop1cycl  32662  satfrnmapom  32895  satf0op  32902  sat1el2xp  32904  dmopab3rexdif  32930  mppspstlem  33096  frrlem2  33434  frrlem3  33435  frrlem4  33436  frrlem8  33440  sslttr  33634  txpss3v  33810  pprodss4v  33816  elsingles  33850  fnimage  33861  funpartlem  33874  funpartfun  33875  dfrdg4  33883  colinearex  33992  bj-cleljusti  34488  axc11n11r  34492  bj-exlimvmpi  34717  bj-snglex  34775  bj-bm1.3ii  34847  bj-restpw  34873  mptsnunlem  35121  ctbssinf  35189  pibt2  35200  wl-moteq  35285  wl-sbcom2d  35328  wl-mo3t  35343  ptrecube  35389  mblfinlem3  35428  ovoliunnfl  35431  voliunnfl  35433  volsupnfl  35434  indexdom  35504  xrnss3v  36114  prtlem16  36495  sbccomieg  40171  setindtr  40402  setindtrs  40403  dfac11  40443  lnmlmic  40469  gicabl  40480  isnumbasgrplem1  40482  iscard4  40678  rtrclex  40754  clcnvlem  40760  brtrclfv2  40865  snhesn  40924  frege55b  41035  frege55c  41056  grucollcld  41404  grumnudlem  41429  iotain  41557  iotavalb  41570  sbiota1  41574  iunconnlem2  42077  fnchoice  42094  stoweidlem59  43126  vitali2  43758  nsssmfmbf  43837  fsetprcnexALT  44078  funop1  44292  sbcpr  44491  opmpoismgm  44879  nzerooringczr  45148  mo0sn  45677  mofmo  45688  neircl  45704  setrec1lem3  45832  elsetrecs  45842  elpglem1  45853