![]() |
Intuitionistic Logic Explorer Theorem List (p. 15 of 95) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Axiom | ax-13 1401 | Axiom of Equality. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the left-hand side of the ∈ binary predicate. Axiom scheme C12' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77. "Non-logical" means that the predicate is not a primitive of predicate calculus proper but instead is an extension to it. "Binary" means that the predicate has two arguments. In a system of predicate calculus with equality, like ours, equality is not usually considered to be a non-logical predicate. In systems of predicate calculus without equality, it typically would be. (Contributed by NM, 5-Aug-1993.) |
⊢ (x = y → (x ∈ z → y ∈ z)) | ||
Axiom | ax-14 1402 | Axiom of Equality. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the right-hand side of the ∈ binary predicate. Axiom scheme C13' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77. (Contributed by NM, 5-Aug-1993.) |
⊢ (x = y → (z ∈ x → z ∈ y)) | ||
Theorem | hbequid 1403 | Bound-variable hypothesis builder for x = x. This theorem tells us that any variable, including x, is effectively not free in x = x, even though x is technically free according to the traditional definition of free variable. (The proof uses only ax-5 1333, ax-8 1392, ax-12 1399, and ax-gen 1335. This shows that this can be proved without ax-9 1421, even though the theorem equid 1586 cannot be. A shorter proof using ax-9 1421 is obtainable from equid 1586 and hbth 1349.) (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 23-Mar-2014.) |
⊢ (x = x → ∀y x = x) | ||
Theorem | axi12 1404 | Proof that ax-i12 1395 follows from ax-bndl 1396. So that we can track which theorems rely on ax-bndl 1396, proofs should reference ax-i12 1395 rather than this theorem. (Contributed by Jim Kingdon, 17-Aug-2018.) (New usage is discouraged). (Proof modification is discouraged.) |
⊢ (∀z z = x ∨ (∀z z = y ∨ ∀z(x = y → ∀z x = y))) | ||
Theorem | alequcom 1405 | Commutation law for identical variable specifiers. The antecedent and consequent are true when x and y are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). (Contributed by NM, 5-Aug-1993.) |
⊢ (∀x x = y → ∀y y = x) | ||
Theorem | alequcoms 1406 | A commutation rule for identical variable specifiers. (Contributed by NM, 5-Aug-1993.) |
⊢ (∀x x = y → φ) ⇒ ⊢ (∀y y = x → φ) | ||
Theorem | nalequcoms 1407 | A commutation rule for distinct variable specifiers. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 2-Feb-2015.) |
⊢ (¬ ∀x x = y → φ) ⇒ ⊢ (¬ ∀y y = x → φ) | ||
Theorem | nfr 1408 | Consequence of the definition of not-free. (Contributed by Mario Carneiro, 26-Sep-2016.) |
⊢ (Ⅎxφ → (φ → ∀xφ)) | ||
Theorem | nfri 1409 | Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎxφ ⇒ ⊢ (φ → ∀xφ) | ||
Theorem | nfrd 1410 | Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (φ → Ⅎxψ) ⇒ ⊢ (φ → (ψ → ∀xψ)) | ||
Theorem | alimd 1411 | Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎxφ & ⊢ (φ → (ψ → χ)) ⇒ ⊢ (φ → (∀xψ → ∀xχ)) | ||
Theorem | alrimi 1412 | Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎxφ & ⊢ (φ → ψ) ⇒ ⊢ (φ → ∀xψ) | ||
Theorem | nfd 1413 | Deduce that x is not free in ψ in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎxφ & ⊢ (φ → (ψ → ∀xψ)) ⇒ ⊢ (φ → Ⅎxψ) | ||
Theorem | nfdh 1414 | Deduce that x is not free in ψ in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ (φ → ∀xφ) & ⊢ (φ → (ψ → ∀xψ)) ⇒ ⊢ (φ → Ⅎxψ) | ||
Theorem | nfrimi 1415 | Moving an antecedent outside Ⅎ. (Contributed by Jim Kingdon, 23-Mar-2018.) |
⊢ Ⅎxφ & ⊢ Ⅎx(φ → ψ) ⇒ ⊢ (φ → Ⅎxψ) | ||
Axiom | ax-17 1416* |
Axiom to quantify a variable over a formula in which it does not occur.
Axiom C5 in [Megill] p. 444 (p. 11 of the
preprint). Also appears as
Axiom B6 (p. 75) of system S2 of [Tarski]
p. 77 and Axiom C5-1 of
[Monk2] p. 113.
(Contributed by NM, 5-Aug-1993.) |
⊢ (φ → ∀xφ) | ||
Theorem | a17d 1417* | ax-17 1416 with antecedent. (Contributed by NM, 1-Mar-2013.) |
⊢ (φ → (ψ → ∀xψ)) | ||
Theorem | nfv 1418* | If x is not present in φ, then x is not free in φ. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎxφ | ||
Theorem | nfvd 1419* | nfv 1418 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1474. (Contributed by Mario Carneiro, 6-Oct-2016.) |
⊢ (φ → Ⅎxψ) | ||
Axiom | ax-i9 1420 | Axiom of Existence. One of the equality and substitution axioms of predicate calculus with equality. One thing this axiom tells us is that at least one thing exists (although ax-4 1397 and possibly others also tell us that, i.e. they are not valid in the empty domain of a "free logic"). In this form (not requiring that x and y be distinct) it was used in an axiom system of Tarski (see Axiom B7' in footnote 1 of [KalishMontague] p. 81.) Another name for this theorem is a9e 1583, which has additional remarks. (Contributed by Mario Carneiro, 31-Jan-2015.) |
⊢ ∃x x = y | ||
Theorem | ax-9 1421 | Derive ax-9 1421 from ax-i9 1420, the modified version for intuitionistic logic. Although ax-9 1421 does hold intuistionistically, in intuitionistic logic it is weaker than ax-i9 1420. (Contributed by NM, 3-Feb-2015.) |
⊢ ¬ ∀x ¬ x = y | ||
Theorem | equidqe 1422 | equid 1586 with some quantification and negation without using ax-4 1397 or ax-17 1416. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) |
⊢ ¬ ∀y ¬ x = x | ||
Theorem | ax4sp1 1423 | A special case of ax-4 1397 without using ax-4 1397 or ax-17 1416. (Contributed by NM, 13-Jan-2011.) |
⊢ (∀y ¬ x = x → ¬ x = x) | ||
Axiom | ax-ial 1424 | x is not free in ∀xφ. Axiom 7 of 10 for intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.) |
⊢ (∀xφ → ∀x∀xφ) | ||
Axiom | ax-i5r 1425 | Axiom of quantifier collection. (Contributed by Mario Carneiro, 31-Jan-2015.) |
⊢ ((∀xφ → ∀xψ) → ∀x(∀xφ → ψ)) | ||
Theorem | spi 1426 | Inference rule reversing generalization. (Contributed by NM, 5-Aug-1993.) |
⊢ ∀xφ ⇒ ⊢ φ | ||
Theorem | sps 1427 | Generalization of antecedent. (Contributed by NM, 5-Aug-1993.) |
⊢ (φ → ψ) ⇒ ⊢ (∀xφ → ψ) | ||
Theorem | spsd 1428 | Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.) |
⊢ (φ → (ψ → χ)) ⇒ ⊢ (φ → (∀xψ → χ)) | ||
Theorem | nfbidf 1429 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.) |
⊢ Ⅎxφ & ⊢ (φ → (ψ ↔ χ)) ⇒ ⊢ (φ → (Ⅎxψ ↔ Ⅎxχ)) | ||
Theorem | hba1 1430 | x is not free in ∀xφ. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 5-Aug-1993.) |
⊢ (∀xφ → ∀x∀xφ) | ||
Theorem | nfa1 1431 | x is not free in ∀xφ. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎx∀xφ | ||
Theorem | a5i 1432 | Inference generalizing a consequent. (Contributed by NM, 5-Aug-1993.) |
⊢ (∀xφ → ψ) ⇒ ⊢ (∀xφ → ∀xψ) | ||
Theorem | nfnf1 1433 | x is not free in Ⅎxφ. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ ℲxℲxφ | ||
Theorem | hbim 1434 | If x is not free in φ and ψ, it is not free in (φ → ψ). (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 3-Mar-2008.) (Revised by Mario Carneiro, 2-Feb-2015.) |
⊢ (φ → ∀xφ) & ⊢ (ψ → ∀xψ) ⇒ ⊢ ((φ → ψ) → ∀x(φ → ψ)) | ||
Theorem | hbor 1435 | If x is not free in φ and ψ, it is not free in (φ ∨ ψ). (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
⊢ (φ → ∀xφ) & ⊢ (ψ → ∀xψ) ⇒ ⊢ ((φ ∨ ψ) → ∀x(φ ∨ ψ)) | ||
Theorem | hban 1436 | If x is not free in φ and ψ, it is not free in (φ ∧ ψ). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.) |
⊢ (φ → ∀xφ) & ⊢ (ψ → ∀xψ) ⇒ ⊢ ((φ ∧ ψ) → ∀x(φ ∧ ψ)) | ||
Theorem | hbbi 1437 | If x is not free in φ and ψ, it is not free in (φ ↔ ψ). (Contributed by NM, 5-Aug-1993.) |
⊢ (φ → ∀xφ) & ⊢ (ψ → ∀xψ) ⇒ ⊢ ((φ ↔ ψ) → ∀x(φ ↔ ψ)) | ||
Theorem | hb3or 1438 | If x is not free in φ, ψ, and χ, it is not free in (φ ∨ ψ ∨ χ). (Contributed by NM, 14-Sep-2003.) |
⊢ (φ → ∀xφ) & ⊢ (ψ → ∀xψ) & ⊢ (χ → ∀xχ) ⇒ ⊢ ((φ ∨ ψ ∨ χ) → ∀x(φ ∨ ψ ∨ χ)) | ||
Theorem | hb3an 1439 | If x is not free in φ, ψ, and χ, it is not free in (φ ∧ ψ ∧ χ). (Contributed by NM, 14-Sep-2003.) |
⊢ (φ → ∀xφ) & ⊢ (ψ → ∀xψ) & ⊢ (χ → ∀xχ) ⇒ ⊢ ((φ ∧ ψ ∧ χ) → ∀x(φ ∧ ψ ∧ χ)) | ||
Theorem | hba2 1440 | Lemma 24 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.) |
⊢ (∀y∀xφ → ∀x∀y∀xφ) | ||
Theorem | hbia1 1441 | Lemma 23 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.) |
⊢ ((∀xφ → ∀xψ) → ∀x(∀xφ → ∀xψ)) | ||
Theorem | 19.3h 1442 | A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 21-May-2007.) |
⊢ (φ → ∀xφ) ⇒ ⊢ (∀xφ ↔ φ) | ||
Theorem | 19.3 1443 | A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎxφ ⇒ ⊢ (∀xφ ↔ φ) | ||
Theorem | 19.16 1444 | Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎxφ ⇒ ⊢ (∀x(φ ↔ ψ) → (φ ↔ ∀xψ)) | ||
Theorem | 19.17 1445 | Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎxψ ⇒ ⊢ (∀x(φ ↔ ψ) → (∀xφ ↔ ψ)) | ||
Theorem | 19.21h 1446 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "x is not free in φ." New proofs should use 19.21 1472 instead. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
⊢ (φ → ∀xφ) ⇒ ⊢ (∀x(φ → ψ) ↔ (φ → ∀xψ)) | ||
Theorem | 19.21bi 1447 | Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
⊢ (φ → ∀xψ) ⇒ ⊢ (φ → ψ) | ||
Theorem | 19.21bbi 1448 | Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.) |
⊢ (φ → ∀x∀yψ) ⇒ ⊢ (φ → ψ) | ||
Theorem | 19.27h 1449 | Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
⊢ (ψ → ∀xψ) ⇒ ⊢ (∀x(φ ∧ ψ) ↔ (∀xφ ∧ ψ)) | ||
Theorem | 19.27 1450 | Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
⊢ Ⅎxψ ⇒ ⊢ (∀x(φ ∧ ψ) ↔ (∀xφ ∧ ψ)) | ||
Theorem | 19.28h 1451 | Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
⊢ (φ → ∀xφ) ⇒ ⊢ (∀x(φ ∧ ψ) ↔ (φ ∧ ∀xψ)) | ||
Theorem | 19.28 1452 | Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
⊢ Ⅎxφ ⇒ ⊢ (∀x(φ ∧ ψ) ↔ (φ ∧ ∀xψ)) | ||
Theorem | nfan1 1453 | A closed form of nfan 1454. (Contributed by Mario Carneiro, 3-Oct-2016.) |
⊢ Ⅎxφ & ⊢ (φ → Ⅎxψ) ⇒ ⊢ Ⅎx(φ ∧ ψ) | ||
Theorem | nfan 1454 | If x is not free in φ and ψ, it is not free in (φ ∧ ψ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) |
⊢ Ⅎxφ & ⊢ Ⅎxψ ⇒ ⊢ Ⅎx(φ ∧ ψ) | ||
Theorem | nf3an 1455 | If x is not free in φ, ψ, and χ, it is not free in (φ ∧ ψ ∧ χ). (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎxφ & ⊢ Ⅎxψ & ⊢ Ⅎxχ ⇒ ⊢ Ⅎx(φ ∧ ψ ∧ χ) | ||
Theorem | nford 1456 | If in a context x is not free in ψ and χ, it is not free in (ψ ∨ χ). (Contributed by Jim Kingdon, 29-Oct-2019.) |
⊢ (φ → Ⅎxψ) & ⊢ (φ → Ⅎxχ) ⇒ ⊢ (φ → Ⅎx(ψ ∨ χ)) | ||
Theorem | nfand 1457 | If in a context x is not free in ψ and χ, it is not free in (ψ ∧ χ). (Contributed by Mario Carneiro, 7-Oct-2016.) |
⊢ (φ → Ⅎxψ) & ⊢ (φ → Ⅎxχ) ⇒ ⊢ (φ → Ⅎx(ψ ∧ χ)) | ||
Theorem | nf3and 1458 | Deduction form of bound-variable hypothesis builder nf3an 1455. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.) |
⊢ (φ → Ⅎxψ) & ⊢ (φ → Ⅎxχ) & ⊢ (φ → Ⅎxθ) ⇒ ⊢ (φ → Ⅎx(ψ ∧ χ ∧ θ)) | ||
Theorem | hbim1 1459 | A closed form of hbim 1434. (Contributed by NM, 5-Aug-1993.) |
⊢ (φ → ∀xφ) & ⊢ (φ → (ψ → ∀xψ)) ⇒ ⊢ ((φ → ψ) → ∀x(φ → ψ)) | ||
Theorem | nfim1 1460 | A closed form of nfim 1461. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
⊢ Ⅎxφ & ⊢ (φ → Ⅎxψ) ⇒ ⊢ Ⅎx(φ → ψ) | ||
Theorem | nfim 1461 | If x is not free in φ and ψ, it is not free in (φ → ψ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
⊢ Ⅎxφ & ⊢ Ⅎxψ ⇒ ⊢ Ⅎx(φ → ψ) | ||
Theorem | hbimd 1462 | Deduction form of bound-variable hypothesis builder hbim 1434. (Contributed by NM, 1-Jan-2002.) (Revised by NM, 2-Feb-2015.) |
⊢ (φ → ∀xφ) & ⊢ (φ → (ψ → ∀xψ)) & ⊢ (φ → (χ → ∀xχ)) ⇒ ⊢ (φ → ((ψ → χ) → ∀x(ψ → χ))) | ||
Theorem | nfor 1463 | If x is not free in φ and ψ, it is not free in (φ ∨ ψ). (Contributed by Jim Kingdon, 11-Mar-2018.) |
⊢ Ⅎxφ & ⊢ Ⅎxψ ⇒ ⊢ Ⅎx(φ ∨ ψ) | ||
Theorem | hbbid 1464 | Deduction form of bound-variable hypothesis builder hbbi 1437. (Contributed by NM, 1-Jan-2002.) |
⊢ (φ → ∀xφ) & ⊢ (φ → (ψ → ∀xψ)) & ⊢ (φ → (χ → ∀xχ)) ⇒ ⊢ (φ → ((ψ ↔ χ) → ∀x(ψ ↔ χ))) | ||
Theorem | nfal 1465 | If x is not free in φ, it is not free in ∀yφ. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎxφ ⇒ ⊢ Ⅎx∀yφ | ||
Theorem | nfnf 1466 | If x is not free in φ, it is not free in Ⅎyφ. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) |
⊢ Ⅎxφ ⇒ ⊢ ℲxℲyφ | ||
Theorem | nfalt 1467 | Closed form of nfal 1465. (Contributed by Jim Kingdon, 11-May-2018.) |
⊢ (∀yℲxφ → Ⅎx∀yφ) | ||
Theorem | nfa2 1468 | Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎx∀y∀xφ | ||
Theorem | nfia1 1469 | Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎx(∀xφ → ∀xψ) | ||
Theorem | 19.21ht 1470 | Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (New usage is discouraged.) |
⊢ (∀x(φ → ∀xφ) → (∀x(φ → ψ) ↔ (φ → ∀xψ))) | ||
Theorem | 19.21t 1471 | Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) |
⊢ (Ⅎxφ → (∀x(φ → ψ) ↔ (φ → ∀xψ))) | ||
Theorem | 19.21 1472 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "x is not free in φ." (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎxφ ⇒ ⊢ (∀x(φ → ψ) ↔ (φ → ∀xψ)) | ||
Theorem | stdpc5 1473 | An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis Ⅎxφ can be thought of as emulating "x is not free in φ." With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example x would not (for us) be free in x = x by nfequid 1587. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. (Contributed by NM, 22-Sep-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
⊢ Ⅎxφ ⇒ ⊢ (∀x(φ → ψ) → (φ → ∀xψ)) | ||
Theorem | nfimd 1474 | If in a context x is not free in ψ and χ, it is not free in (ψ → χ). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) |
⊢ (φ → Ⅎxψ) & ⊢ (φ → Ⅎxχ) ⇒ ⊢ (φ → Ⅎx(ψ → χ)) | ||
Theorem | aaanh 1475 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |
⊢ (φ → ∀yφ) & ⊢ (ψ → ∀xψ) ⇒ ⊢ (∀x∀y(φ ∧ ψ) ↔ (∀xφ ∧ ∀yψ)) | ||
Theorem | aaan 1476 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |
⊢ Ⅎyφ & ⊢ Ⅎxψ ⇒ ⊢ (∀x∀y(φ ∧ ψ) ↔ (∀xφ ∧ ∀yψ)) | ||
Theorem | nfbid 1477 | If in a context x is not free in ψ and χ, it is not free in (ψ ↔ χ). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.) |
⊢ (φ → Ⅎxψ) & ⊢ (φ → Ⅎxχ) ⇒ ⊢ (φ → Ⅎx(ψ ↔ χ)) | ||
Theorem | nfbi 1478 | If x is not free in φ and ψ, it is not free in (φ ↔ ψ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
⊢ Ⅎxφ & ⊢ Ⅎxψ ⇒ ⊢ Ⅎx(φ ↔ ψ) | ||
Theorem | 19.8a 1479 | If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
⊢ (φ → ∃xφ) | ||
Theorem | 19.23bi 1480 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
⊢ (∃xφ → ψ) ⇒ ⊢ (φ → ψ) | ||
Theorem | exlimih 1481 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ (ψ → ∀xψ) & ⊢ (φ → ψ) ⇒ ⊢ (∃xφ → ψ) | ||
Theorem | exlimi 1482 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎxψ & ⊢ (φ → ψ) ⇒ ⊢ (∃xφ → ψ) | ||
Theorem | exlimd2 1483 | Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1484 but with one slightly different hypothesis. (Contributed by Jim Kingdon, 30-Dec-2017.) |
⊢ (φ → ∀xφ) & ⊢ (φ → (χ → ∀xχ)) & ⊢ (φ → (ψ → χ)) ⇒ ⊢ (φ → (∃xψ → χ)) | ||
Theorem | exlimdh 1484 | Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.) |
⊢ (φ → ∀xφ) & ⊢ (χ → ∀xχ) & ⊢ (φ → (ψ → χ)) ⇒ ⊢ (φ → (∃xψ → χ)) | ||
Theorem | exlimd 1485 | Deduction from Theorem 19.9 of [Margaris] p. 89. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof rewritten by Jim Kingdon, 18-Jun-2018.) |
⊢ Ⅎxφ & ⊢ Ⅎxχ & ⊢ (φ → (ψ → χ)) ⇒ ⊢ (φ → (∃xψ → χ)) | ||
Theorem | exlimiv 1486* |
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.) |
⊢ (φ → ψ) ⇒ ⊢ (∃xφ → ψ) | ||
Theorem | exim 1487 | Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
⊢ (∀x(φ → ψ) → (∃xφ → ∃xψ)) | ||
Theorem | eximi 1488 | Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.) |
⊢ (φ → ψ) ⇒ ⊢ (∃xφ → ∃xψ) | ||
Theorem | 2eximi 1489 | Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
⊢ (φ → ψ) ⇒ ⊢ (∃x∃yφ → ∃x∃yψ) | ||
Theorem | eximii 1490 | Inference associated with eximi 1488. (Contributed by BJ, 3-Feb-2018.) |
⊢ ∃xφ & ⊢ (φ → ψ) ⇒ ⊢ ∃xψ | ||
Theorem | alinexa 1491 | A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.) |
⊢ (∀x(φ → ¬ ψ) ↔ ¬ ∃x(φ ∧ ψ)) | ||
Theorem | exbi 1492 | Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
⊢ (∀x(φ ↔ ψ) → (∃xφ ↔ ∃xψ)) | ||
Theorem | exbii 1493 | Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.) |
⊢ (φ ↔ ψ) ⇒ ⊢ (∃xφ ↔ ∃xψ) | ||
Theorem | 2exbii 1494 | Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |
⊢ (φ ↔ ψ) ⇒ ⊢ (∃x∃yφ ↔ ∃x∃yψ) | ||
Theorem | 3exbii 1495 | Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.) |
⊢ (φ ↔ ψ) ⇒ ⊢ (∃x∃y∃zφ ↔ ∃x∃y∃zψ) | ||
Theorem | exancom 1496 | Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.) |
⊢ (∃x(φ ∧ ψ) ↔ ∃x(ψ ∧ φ)) | ||
Theorem | alrimdd 1497 | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎxφ & ⊢ (φ → Ⅎxψ) & ⊢ (φ → (ψ → χ)) ⇒ ⊢ (φ → (ψ → ∀xχ)) | ||
Theorem | alrimd 1498 | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎxφ & ⊢ Ⅎxψ & ⊢ (φ → (ψ → χ)) ⇒ ⊢ (φ → (ψ → ∀xχ)) | ||
Theorem | eximdh 1499 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.) |
⊢ (φ → ∀xφ) & ⊢ (φ → (ψ → χ)) ⇒ ⊢ (φ → (∃xψ → ∃xχ)) | ||
Theorem | eximd 1500 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎxφ & ⊢ (φ → (ψ → χ)) ⇒ ⊢ (φ → (∃xψ → ∃xχ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |