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  5829  funop  5830  funopdmsn  5833  eusvobj2  6003  acexmidlemv  6015  fnoprabg  6121  fo1stresm  6323  fo2ndresm  6324  eloprabi  6360  cnvoprab  6398  reldmtpos  6418  dftpos4  6428  tfrlem9  6484  tfrexlem  6499  ecdmn0m  6745  mapprc  6820  ixpprc  6887  ixpm  6898  bren  6916  brdomg  6918  domssr  6950  ener  6952  en0  6968  en1  6972  en1bg  6973  2dom  6979  fiprc  6989  dom1o  7001  enm  7003  ssenen  7036  php5dom  7048  ssfilem  7061  ssfilemd  7063  diffitest  7075  inffiexmid  7097  ctm  7307  ctssdclemr  7310  ctssdc  7311  enumct  7313  ctfoex  7316  ctssexmid  7348  pm54.43  7394  pr2cv1  7399  acnrcl  7415  subhalfnqq  7633  nqnq0pi  7657  nqnq0  7660  prarloc  7722  nqprm  7761  ltexprlemm  7819  recexprlemell  7841  recexprlemelu  7842  recexprlemopl  7844  recexprlemopu  7846  recexprlempr  7851  sup3exmid  9136  fzm  10272  fzom  10399  fclim  11854  climmo  11858  nninfct  12611  ctinfom  13048  qnnen  13051  unct  13062  omiunct  13064  opifismgmdc  13453  ismgmid  13459  gsumval2  13479  ismnd  13501  dfgrp2e  13610  dfgrp3me  13682  subgintm  13784  zrhval  14630  topnex  14809  edgval  15910  upgrex  15953  g0wlk0  16220  clwwlknonmpo  16278  bdbm1.3ii  16486  domomsubct  16602