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  7450  ctssdclemr  7453  ctssdc  7454  enumct  7456  ctfoex  7459  ctssexmid  7491  pm54.43  7537  pr2cv1  7542  acnrcl  7558  subhalfnqq  7782  nqnq0pi  7806  nqnq0  7809  prarloc  7871  nqprm  7910  ltexprlemm  7968  recexprlemell  7990  recexprlemelu  7991  recexprlemopl  7993  recexprlemopu  7995  recexprlempr  8000  sup3exmid  9290  indval0  9300  fzm  10453  fzom  10583  hashf1lem2  11302  fclim  12079  climmo  12083  nninfct  12837  ctinfom  13371  qnnen  13374  unct  13385  omiunct  13387  opifismgmdc  13744  ismgmid  13750  gzsumval2  13767  ismnd  13785  dfgrp2e  13886  dfgrp3me  13958  subgintm  14054  cntrval  14145  cntzval  14147  cntzrcl  14153  resscntz  14160  mgpplusg  14306  mgpbas  14309  ringidval  14349  zrhval  15036  asclfval  15105  topnex  15278  edgval  16467  upgrex  16510  g0wlk0  16777  clwwlknonmpo  16835  bdbm1.3ii  17083  domomsubct  17197  wexmiddiffilem  17209  wexmiddifxylem  17211