Theorem exlimiv 1644

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

Syntax hints:   → wi 4  ∃wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1495  ax-ie2 1540  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1873  ax11ev  1874  equs5or  1876  exlimivv  1943  cbvexvw  1967  mo23  2119  mopick  2156  gencl  2832  cgsexg  2835  gencbvex2  2848  vtocleg  2874  eqvinc  2926  eqvincg  2927  elrabi  2956  sbcex2  3082  oprcl  3881  eluni  3891  intab  3952  uniintsnr  3959  trintssm  4198  bm1.3ii  4205  inteximm  4233  axpweq  4255  bnd2  4257  unipw  4303  euabex  4311  mss  4312  exss  4313  opelopabsb  4348  eusvnf  4544  eusvnfb  4545  regexmidlem1  4625  eunex  4653  relop  4872  dmrnssfld  4987  xpmlem  5149  dmxpss  5159  dmsnopg  5200  elxp5  5217  iotauni  5291  iota1  5293  iota4  5298  iotam  5310  funimaexglem  5404  ffoss  5606  relelfvdm  5661  elfvm  5662  nfvres  5665  fvelrnb  5683  funopsn  5819  funop  5820  funopdmsn  5823  eusvobj2  5993  acexmidlemv  6005  fnoprabg  6111  fo1stresm  6313  fo2ndresm  6314  eloprabi  6348  cnvoprab  6386  reldmtpos  6405  dftpos4  6415  tfrlem9  6471  tfrexlem  6486  ecdmn0m  6732  mapprc  6807  ixpprc  6874  ixpm  6885  bren  6903  brdomg  6905  domssr  6937  ener  6939  en0  6955  en1  6959  en1bg  6960  2dom  6966  fiprc  6976  dom1o  6985  enm  6987  ssenen  7020  php5dom  7032  ssfilem  7045  diffitest  7057  inffiexmid  7079  ctm  7287  ctssdclemr  7290  ctssdc  7291  enumct  7293  ctfoex  7296  ctssexmid  7328  pm54.43  7374  pr2cv1  7379  acnrcl  7394  subhalfnqq  7612  nqnq0pi  7636  nqnq0  7639  prarloc  7701  nqprm  7740  ltexprlemm  7798  recexprlemell  7820  recexprlemelu  7821  recexprlemopl  7823  recexprlemopu  7825  recexprlempr  7830  sup3exmid  9115  fzm  10246  fzom  10373  fclim  11820  climmo  11824  nninfct  12577  ctinfom  13014  qnnen  13017  unct  13028  omiunct  13030  opifismgmdc  13419  ismgmid  13425  gsumval2  13445  ismnd  13467  dfgrp2e  13576  dfgrp3me  13648  subgintm  13750  zrhval  14596  topnex  14775  upgrex  15918  g0wlk0  16111  bdbm1.3ii  16309  domomsubct  16426