Theorem exlimiv 1471

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 1471 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 1400	. 2 ⊢ (ψ → ∀xψ)
2		exlimiv.1	. 2 ⊢ (φ → ψ)
3	1, 2	exlimih 1466	1 ⊢ (∃xφ → ψ)

Syntax hints:   → wi 4  ∃wex 1362

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1318  ax-ie2 1364  ax-17 1400

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ax11v  1690  ax11ev  1691  equs5or  1693  exlimivv  1758  mo23  1923  mopick  1960  gencl  2563  cgsexg  2566  gencbvex2  2578  vtocleg  2601  eqvinc  2644  eqvincg  2645  elrabi  2672  sbcex2  2789  oprcl  3547  eluni  3557  intab  3618  uniintsnr  3625  trint0m  3845  bm1.3ii  3852  inteximm  3877  axpweq  3898  bnd2  3900  unipw  3927  euabex  3935  mss  3936  exss  3937  opelopabsb  3971  eusvnf  4135  eusvnfb  4136  regexmidlem1  4202  eunex  4223  relop  4413  dmrnssfld  4522  xpmlem  4671  dmxpss  4680  dmsnopg  4719  elxp5  4736  iotauni  4806  iota1  4808  iota4  4812  funimaexglem  4908  ffoss  5083  relelfvdm  5130  nfvres  5131  fvelrnb  5146  eusvobj2  5422  acexmidlemv  5434  fnoprabg  5525  fo1stresm  5711  fo2ndresm  5712  eloprabi  5745  reldmtpos  5790  dftpos4  5800  tfrlem9  5857  tfrexlem  5870  ecdmn0m  6059  subhalfnqq  6271  nqnq0pi  6293  nqnq0  6296  prarloc  6357  nqprm  6397  ltexprlemm  6437  recexprlemell  6456  recexprlemelu  6457  recexprlemopl  6459  recexprlemopu  6461  recexprlempr  6466  bdbm1.3ii  7117