Theorem exlimiv 1651

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  ax11v  1880  ax11ev  1881  equs5or  1883  exlimivv  1952  cbvexvw  1976  mo23  2128  mopick  2165  gencl  2854  cgsexg  2857  gencbvex2  2870  vtocleg  2896  eqvinc  2949  eqvincg  2950  elrabi  2979  sbcex2  3105  oprcl  3928  eluni  3938  intab  3999  uniintsnr  4006  trintssm  4245  bm1.3ii  4254  inteximm  4285  axpweq  4308  bnd2  4310  unipw  4357  euabex  4365  mss  4366  exss  4367  opelopabsb  4402  eusvnf  4599  eusvnfb  4600  regexmidlem1  4680  eunex  4708  relop  4930  dmrnssfld  5045  xpmlem  5208  dmxpss  5218  dmsnopg  5259  elxp5  5276  iotauni  5350  iota1  5352  iota4  5357  iotam  5369  funimaexglem  5464  ffoss  5672  relelfvdm  5727  elfvm  5729  nfvres  5732  fvelrnb  5750  funopsn  5891  funop  5892  funopdmsn  5895  mptmex  5945  eusvobj2  6071  acexmidlemv  6083  fnoprabg  6189  fo1stresm  6395  fo2ndresm  6396  eloprabi  6432  cnvoprab  6470  reldmtpos  6524  dftpos4  6534  tfrlem9  6590  tfrexlem  6605  ecdmn0m  6851  mapprc  6926  ixpprc  7001  ixpm  7012  bren  7030  brdomg  7032  domssr  7064  ener  7066  en0  7082  en1  7086  en1bg  7087  2dom  7093  fiprc  7104  dom1o  7116  enm  7118  ssenen  7152  php5dom  7164  ssfilem  7177  ssfilemd  7179  diffitest  7191  inffiexmid  7213  ctm  7449  ctssdclemr  7452  ctssdc  7453  enumct  7455  ctfoex  7458  ctssexmid  7490  pm54.43  7536  pr2cv1  7541  acnrcl  7557  subhalfnqq  7781  nqnq0pi  7805  nqnq0  7808  prarloc  7870  nqprm  7909  ltexprlemm  7967  recexprlemell  7989  recexprlemelu  7990  recexprlemopl  7992  recexprlemopu  7994  recexprlempr  7999  sup3exmid  9289  indval0  9299  fzm  10452  fzom  10582  hashf1lem2  11300  fclim  12076  climmo  12080  nninfct  12834  ctinfom  13368  qnnen  13371  unct  13382  omiunct  13384  opifismgmdc  13740  ismgmid  13746  gzsumval2  13763  ismnd  13781  dfgrp2e  13882  dfgrp3me  13954  subgintm  14050  mgpplusg  14271  mgpbas  14274  ringidval  14314  zrhval  15001  asclfval  15070  topnex  15236  edgval  16399  upgrex  16442  g0wlk0  16709  clwwlknonmpo  16767  bdbm1.3ii  17015  domomsubct  17129  wexmiddiffilem  17141  wexmiddifxylem  17143