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  3564  eluni  3574  intab  3635  uniintsnr  3642  trint0m  3862  bm1.3ii  3869  inteximm  3894  axpweq  3915  bnd2  3917  unipw  3944  euabex  3952  mss  3953  exss  3954  opelopabsb  3988  eusvnf  4151  eusvnfb  4152  regexmidlem1  4218  eunex  4239  relop  4429  dmrnssfld  4538  xpmlem  4687  dmxpss  4696  dmsnopg  4735  elxp5  4752  iotauni  4822  iota1  4824  iota4  4828  funimaexglem  4925  ffoss  5101  relelfvdm  5148  nfvres  5149  fvelrnb  5164  eusvobj2  5441  acexmidlemv  5453  fnoprabg  5544  fo1stresm  5730  fo2ndresm  5731  eloprabi  5764  reldmtpos  5809  dftpos4  5819  tfrlem9  5876  tfrexlem  5889  ecdmn0m  6084  bren  6164  brdomg  6165  ener  6195  en0  6211  en1  6215  en1bg  6216  2dom  6221  fiprc  6228  enm  6230  ssfiexmid  6254  subhalfnqq  6397  nqnq0pi  6421  nqnq0  6424  prarloc  6486  nqprm  6525  ltexprlemm  6574  recexprlemell  6594  recexprlemelu  6595  recexprlemopl  6597  recexprlemopu  6599  recexprlempr  6604  fzm  8672  fzom  8790  bdbm1.3ii  9346