Theorem exlimiv 1622

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 1622 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 1550	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
2		exlimiv.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	exlimih 1617	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1473  ax-ie2 1518  ax-17 1550

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1851  ax11ev  1852  equs5or  1854  exlimivv  1921  cbvexvw  1945  mo23  2096  mopick  2133  gencl  2806  cgsexg  2809  gencbvex2  2822  vtocleg  2848  eqvinc  2900  eqvincg  2901  elrabi  2930  sbcex2  3056  oprcl  3849  eluni  3859  intab  3920  uniintsnr  3927  trintssm  4166  bm1.3ii  4173  inteximm  4201  axpweq  4223  bnd2  4225  unipw  4269  euabex  4277  mss  4278  exss  4279  opelopabsb  4314  eusvnf  4508  eusvnfb  4509  regexmidlem1  4589  eunex  4617  relop  4836  dmrnssfld  4950  xpmlem  5112  dmxpss  5122  dmsnopg  5163  elxp5  5180  iotauni  5253  iota1  5255  iota4  5260  iotam  5272  funimaexglem  5366  ffoss  5566  relelfvdm  5621  elfvm  5622  nfvres  5623  fvelrnb  5639  funopsn  5775  funop  5776  funopdmsn  5777  eusvobj2  5943  acexmidlemv  5955  fnoprabg  6059  fo1stresm  6260  fo2ndresm  6261  eloprabi  6295  cnvoprab  6333  reldmtpos  6352  dftpos4  6362  tfrlem9  6418  tfrexlem  6433  ecdmn0m  6677  mapprc  6752  ixpprc  6819  ixpm  6830  bren  6848  brdomg  6850  domssr  6882  ener  6884  en0  6900  en1  6904  en1bg  6905  2dom  6911  fiprc  6921  enm  6930  ssenen  6963  php5dom  6975  ssfilem  6987  diffitest  6999  inffiexmid  7018  ctm  7226  ctssdclemr  7229  ctssdc  7230  enumct  7232  ctfoex  7235  ctssexmid  7267  pm54.43  7313  acnrcl  7329  subhalfnqq  7547  nqnq0pi  7571  nqnq0  7574  prarloc  7636  nqprm  7675  ltexprlemm  7733  recexprlemell  7755  recexprlemelu  7756  recexprlemopl  7758  recexprlemopu  7760  recexprlempr  7765  sup3exmid  9050  fzm  10180  fzom  10307  fclim  11680  climmo  11684  nninfct  12437  ctinfom  12874  qnnen  12877  unct  12888  omiunct  12890  opifismgmdc  13278  ismgmid  13284  gsumval2  13304  ismnd  13326  dfgrp2e  13435  dfgrp3me  13507  subgintm  13609  zrhval  14454  topnex  14633  upgrex  15774  bdbm1.3ii  15965  dom1o  16067  domomsubct  16079