Theorem exlimiv 1486

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 x exists satisfying a wff, i.e. ∃xφ(x) where φ(x) has x 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 x) 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 x. Then we apply exlimiv 1486 to arrive at (∃xφ → ψ). Finally, we separately prove ∃xφ and detach it with modus ponens ax-mp 7 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	⊢ (∃xφ → ψ)

Distinct variable group:   ψ,x

Allowed substitution hint:   φ(x)

Proof of Theorem exlimiv

Step	Hyp	Ref	Expression
1		ax-17 1416	. 2 ⊢ (ψ → ∀xψ)
2		exlimiv.1	. 2 ⊢ (φ → ψ)
3	1, 2	exlimih 1481	1 ⊢ (∃xφ → ψ)

Syntax hints:   → wi 4  ∃wex 1378

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1335  ax-ie2 1380  ax-17 1416

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ax11v  1705  ax11ev  1706  equs5or  1708  exlimivv  1773  mo23  1938  mopick  1975  gencl  2580  cgsexg  2583  gencbvex2  2595  vtocleg  2618  eqvinc  2661  eqvincg  2662  elrabi  2689  sbcex2  2806  oprcl  3563  eluni  3573  intab  3634  uniintsnr  3641  trint0m  3861  bm1.3ii  3868  inteximm  3893  axpweq  3914  bnd2  3916  unipw  3943  euabex  3951  mss  3952  exss  3953  opelopabsb  3987  eusvnf  4150  eusvnfb  4151  regexmidlem1  4217  eunex  4238  relop  4428  dmrnssfld  4537  xpmlem  4686  dmxpss  4695  dmsnopg  4734  elxp5  4751  iotauni  4821  iota1  4823  iota4  4827  funimaexglem  4923  ffoss  5099  relelfvdm  5146  nfvres  5147  fvelrnb  5162  eusvobj2  5438  acexmidlemv  5450  fnoprabg  5541  fo1stresm  5727  fo2ndresm  5728  eloprabi  5761  reldmtpos  5806  dftpos4  5816  tfrlem9  5873  tfrexlem  5886  ecdmn0m  6077  bren  6157  brdomg  6158  ener  6188  en0  6204  en1  6208  en1bg  6209  2dom  6214  fiprc  6221  enm  6223  ssfiexmid  6247  subhalfnqq  6390  nqnq0pi  6413  nqnq0  6416  prarloc  6478  nqprm  6518  ltexprlemm  6564  recexprlemell  6584  recexprlemelu  6585  recexprlemopl  6587  recexprlemopu  6589  recexprlempr  6594  fzm  8620  fzom  8736  bdbm1.3ii  8944