Theorem exlimiv 1646

Description: Inference from Theorem 19.23 of [Margaris] p. 90.

This inference, along with our many variants 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.mathsci.appstate.edu/~jlh/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 𝑥 exists satisfying a wff, i.e. ∃𝑥𝜑(𝑥) where 𝜑(𝑥) has 𝑥 free, then we can use 𝜑( C ) as a hypothesis for the proof where C is a new (ficticious) 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 1646 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, 5-Aug-1993.) (Revised by NM, 25-Jul-2012.)

Hypothesis

Ref	Expression
exlimiv.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
exlimiv	⊢ (∃𝑥𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem exlimiv

Step	Hyp	Ref	Expression
1		ax-17 1574	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
2		exlimiv.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	exlimih 1641	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1497  ax-ie2 1542  ax-17 1574

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1875  ax11ev  1876  equs5or  1878  exlimivv  1945  cbvexvw  1969  mo23  2121  mopick  2158  gencl  2835  cgsexg  2838  gencbvex2  2851  vtocleg  2877  eqvinc  2929  eqvincg  2930  elrabi  2959  sbcex2  3085  oprcl  3886  eluni  3896  intab  3957  uniintsnr  3964  trintssm  4203  bm1.3ii  4210  inteximm  4239  axpweq  4261  bnd2  4263  unipw  4309  euabex  4317  mss  4318  exss  4319  opelopabsb  4354  eusvnf  4550  eusvnfb  4551  regexmidlem1  4631  eunex  4659  relop  4880  dmrnssfld  4995  xpmlem  5157  dmxpss  5167  dmsnopg  5208  elxp5  5225  iotauni  5299  iota1  5301  iota4  5306  iotam  5318  funimaexglem  5413  ffoss  5616  relelfvdm  5671  elfvm  5672  nfvres  5675  fvelrnb  5693  funopsn  5830  funop  5831  funopdmsn  5834  eusvobj2  6004  acexmidlemv  6016  fnoprabg  6122  fo1stresm  6324  fo2ndresm  6325  eloprabi  6361  cnvoprab  6399  reldmtpos  6419  dftpos4  6429  tfrlem9  6485  tfrexlem  6500  ecdmn0m  6746  mapprc  6821  ixpprc  6888  ixpm  6899  bren  6917  brdomg  6919  domssr  6951  ener  6953  en0  6969  en1  6973  en1bg  6974  2dom  6980  fiprc  6990  dom1o  7002  enm  7004  ssenen  7037  php5dom  7049  ssfilem  7062  ssfilemd  7064  diffitest  7076  inffiexmid  7098  ctm  7308  ctssdclemr  7311  ctssdc  7312  enumct  7314  ctfoex  7317  ctssexmid  7349  pm54.43  7395  pr2cv1  7400  acnrcl  7416  subhalfnqq  7634  nqnq0pi  7658  nqnq0  7661  prarloc  7723  nqprm  7762  ltexprlemm  7820  recexprlemell  7842  recexprlemelu  7843  recexprlemopl  7845  recexprlemopu  7847  recexprlempr  7852  sup3exmid  9137  fzm  10273  fzom  10400  fclim  11859  climmo  11863  nninfct  12617  ctinfom  13054  qnnen  13057  unct  13068  omiunct  13070  opifismgmdc  13459  ismgmid  13465  gsumval2  13485  ismnd  13507  dfgrp2e  13616  dfgrp3me  13688  subgintm  13790  zrhval  14637  topnex  14816  edgval  15917  upgrex  15960  g0wlk0  16227  clwwlknonmpo  16285  bdbm1.3ii  16512  domomsubct  16628