Home Intuitionistic Logic ExplorerTheorem List (p. 28 of 110) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 2701-2800   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremrspccva 2701* Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
(𝑥 = 𝐴 → (𝜑𝜓))       ((∀𝑥𝐵 𝜑𝐴𝐵) → 𝜓)

Theoremrspcev 2702* Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
(𝑥 = 𝐴 → (𝜑𝜓))       ((𝐴𝐵𝜓) → ∃𝑥𝐵 𝜑)

Theoremrspcimdv 2703* Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
(𝜑𝐴𝐵)    &   ((𝜑𝑥 = 𝐴) → (𝜓𝜒))       (𝜑 → (∀𝑥𝐵 𝜓𝜒))

Theoremrspcimedv 2704* Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
(𝜑𝐴𝐵)    &   ((𝜑𝑥 = 𝐴) → (𝜒𝜓))       (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))

Theoremrspcdv 2705* Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
(𝜑𝐴𝐵)    &   ((𝜑𝑥 = 𝐴) → (𝜓𝜒))       (𝜑 → (∀𝑥𝐵 𝜓𝜒))

Theoremrspcedv 2706* Restricted existential specialization, using implicit substitution. (Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
(𝜑𝐴𝐵)    &   ((𝜑𝑥 = 𝐴) → (𝜓𝜒))       (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))

Theoremrspcda 2707* Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 29-Jun-2020.)
(𝑥 = 𝐶 → (𝜓𝜒))    &   (𝜑 → ∀𝑥𝐴 𝜓)    &   (𝜑𝐶𝐴)    &   𝑥𝜑       (𝜑𝜒)

Theoremrspcdva 2708* Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.)
(𝑥 = 𝐶 → (𝜓𝜒))    &   (𝜑 → ∀𝑥𝐴 𝜓)    &   (𝜑𝐶𝐴)       (𝜑𝜒)

Theoremrspcedvd 2709* Restricted existential specialization, using implicit substitution. Variant of rspcedv 2706. (Contributed by AV, 27-Nov-2019.)
(𝜑𝐴𝐵)    &   ((𝜑𝑥 = 𝐴) → (𝜓𝜒))    &   (𝜑𝜒)       (𝜑 → ∃𝑥𝐵 𝜓)

Theoremrspcedeq1vd 2710* Restricted existential specialization, using implicit substitution. Variant of rspcedvd 2709 for equations, in which the left hand side depends on the quantified variable. (Contributed by AV, 24-Dec-2019.)
(𝜑𝐴𝐵)    &   ((𝜑𝑥 = 𝐴) → 𝐶 = 𝐷)       (𝜑 → ∃𝑥𝐵 𝐶 = 𝐷)

Theoremrspcedeq2vd 2711* Restricted existential specialization, using implicit substitution. Variant of rspcedvd 2709 for equations, in which the right hand side depends on the quantified variable. (Contributed by AV, 24-Dec-2019.)
(𝜑𝐴𝐵)    &   ((𝜑𝑥 = 𝐴) → 𝐶 = 𝐷)       (𝜑 → ∃𝑥𝐵 𝐶 = 𝐷)

Theoremrspc2 2712* 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 9-Nov-2012.)
𝑥𝜒    &   𝑦𝜓    &   (𝑥 = 𝐴 → (𝜑𝜒))    &   (𝑦 = 𝐵 → (𝜒𝜓))       ((𝐴𝐶𝐵𝐷) → (∀𝑥𝐶𝑦𝐷 𝜑𝜓))

Theoremrspc2gv 2713* Restricted specialization with two quantifiers, using implicit substitution. (Contributed by BJ, 2-Dec-2021.)
((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))       ((𝐴𝑉𝐵𝑊) → (∀𝑥𝑉𝑦𝑊 𝜑𝜓))

Theoremrspc2v 2714* 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.)
(𝑥 = 𝐴 → (𝜑𝜒))    &   (𝑦 = 𝐵 → (𝜒𝜓))       ((𝐴𝐶𝐵𝐷) → (∀𝑥𝐶𝑦𝐷 𝜑𝜓))

Theoremrspc2va 2715* 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.)
(𝑥 = 𝐴 → (𝜑𝜒))    &   (𝑦 = 𝐵 → (𝜒𝜓))       (((𝐴𝐶𝐵𝐷) ∧ ∀𝑥𝐶𝑦𝐷 𝜑) → 𝜓)

Theoremrspc2ev 2716* 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)
(𝑥 = 𝐴 → (𝜑𝜒))    &   (𝑦 = 𝐵 → (𝜒𝜓))       ((𝐴𝐶𝐵𝐷𝜓) → ∃𝑥𝐶𝑦𝐷 𝜑)

Theoremrspc3v 2717* 3-variable restricted specialization, using implicit substitution. (Contributed by NM, 10-May-2005.)
(𝑥 = 𝐴 → (𝜑𝜒))    &   (𝑦 = 𝐵 → (𝜒𝜃))    &   (𝑧 = 𝐶 → (𝜃𝜓))       ((𝐴𝑅𝐵𝑆𝐶𝑇) → (∀𝑥𝑅𝑦𝑆𝑧𝑇 𝜑𝜓))

Theoremrspc3ev 2718* 3-variable restricted existentional specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012.)
(𝑥 = 𝐴 → (𝜑𝜒))    &   (𝑦 = 𝐵 → (𝜒𝜃))    &   (𝑧 = 𝐶 → (𝜃𝜓))       (((𝐴𝑅𝐵𝑆𝐶𝑇) ∧ 𝜓) → ∃𝑥𝑅𝑦𝑆𝑧𝑇 𝜑)

Theoremeqvinc 2719* A variable introduction law for class equality. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
𝐴 ∈ V       (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥 = 𝐵))

Theoremeqvincg 2720* A variable introduction law for class equality, deduction version. (Contributed by Thierry Arnoux, 2-Mar-2017.)
(𝐴𝑉 → (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥 = 𝐵)))

Theoremeqvincf 2721 A variable introduction law for class equality, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Sep-2003.)
𝑥𝐴    &   𝑥𝐵    &   𝐴 ∈ V       (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥 = 𝐵))

Theoremalexeq 2722* Two ways to express substitution of 𝐴 for 𝑥 in 𝜑. (Contributed by NM, 2-Mar-1995.)
𝐴 ∈ V       (∀𝑥(𝑥 = 𝐴𝜑) ↔ ∃𝑥(𝑥 = 𝐴𝜑))

Theoremceqex 2723* Equality implies equivalence with substitution. (Contributed by NM, 2-Mar-1995.)
(𝑥 = 𝐴 → (𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)))

Theoremceqsexg 2724* A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 11-Oct-2004.)
𝑥𝜓    &   (𝑥 = 𝐴 → (𝜑𝜓))       (𝐴𝑉 → (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓))

Theoremceqsexgv 2725* Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 29-Dec-1996.)
(𝑥 = 𝐴 → (𝜑𝜓))       (𝐴𝑉 → (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓))

Theoremceqsrexv 2726* Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004.)
(𝑥 = 𝐴 → (𝜑𝜓))       (𝐴𝐵 → (∃𝑥𝐵 (𝑥 = 𝐴𝜑) ↔ 𝜓))

Theoremceqsrexbv 2727* Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by Mario Carneiro, 14-Mar-2014.)
(𝑥 = 𝐴 → (𝜑𝜓))       (∃𝑥𝐵 (𝑥 = 𝐴𝜑) ↔ (𝐴𝐵𝜓))

Theoremceqsrex2v 2728* Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 29-Oct-2005.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑦 = 𝐵 → (𝜓𝜒))       ((𝐴𝐶𝐵𝐷) → (∃𝑥𝐶𝑦𝐷 ((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝜑) ↔ 𝜒))

Theoremclel2 2729* An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.)
𝐴 ∈ V       (𝐴𝐵 ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵))

Theoremclel3g 2730* An alternate definition of class membership when the class is a set. (Contributed by NM, 13-Aug-2005.)
(𝐵𝑉 → (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐵𝐴𝑥)))

Theoremclel3 2731* An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.)
𝐵 ∈ V       (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐵𝐴𝑥))

Theoremclel4 2732* An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.)
𝐵 ∈ V       (𝐴𝐵 ↔ ∀𝑥(𝑥 = 𝐵𝐴𝑥))

Theorempm13.183 2733* Compare theorem *13.183 in [WhiteheadRussell] p. 178. Only 𝐴 is required to be a set. (Contributed by Andrew Salmon, 3-Jun-2011.)
(𝐴𝑉 → (𝐴 = 𝐵 ↔ ∀𝑧(𝑧 = 𝐴𝑧 = 𝐵)))

Theoremrr19.3v 2734* Restricted quantifier version of Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 25-Oct-2012.)
(∀𝑥𝐴𝑦𝐴 𝜑 ↔ ∀𝑥𝐴 𝜑)

Theoremrr19.28v 2735* Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 29-Oct-2012.)
(∀𝑥𝐴𝑦𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴 (𝜑 ∧ ∀𝑦𝐴 𝜓))

Theoremelabgt 2736* Membership in a class abstraction, using implicit substitution. (Closed theorem version of elabg 2740.) (Contributed by NM, 7-Nov-2005.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
((𝐴𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑𝜓))) → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))

Theoremelabgf 2737 Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) (Revised by Mario Carneiro, 12-Oct-2016.)
𝑥𝐴    &   𝑥𝜓    &   (𝑥 = 𝐴 → (𝜑𝜓))       (𝐴𝐵 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))

Theoremelabf 2738* Membership in a class abstraction, using implicit substitution. (Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro, 12-Oct-2016.)
𝑥𝜓    &   𝐴 ∈ V    &   (𝑥 = 𝐴 → (𝜑𝜓))       (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)

Theoremelab 2739* Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 1-Aug-1994.)
𝐴 ∈ V    &   (𝑥 = 𝐴 → (𝜑𝜓))       (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)

Theoremelabg 2740* Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.)
(𝑥 = 𝐴 → (𝜑𝜓))       (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))

Theoremelab2g 2741* Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   𝐵 = {𝑥𝜑}       (𝐴𝑉 → (𝐴𝐵𝜓))

Theoremelab2 2742* Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
𝐴 ∈ V    &   (𝑥 = 𝐴 → (𝜑𝜓))    &   𝐵 = {𝑥𝜑}       (𝐴𝐵𝜓)

Theoremelab4g 2743* Membership in a class abstraction, using implicit substitution. (Contributed by NM, 17-Oct-2012.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   𝐵 = {𝑥𝜑}       (𝐴𝐵 ↔ (𝐴 ∈ V ∧ 𝜓))

Theoremelab3gf 2744 Membership in a class abstraction, with a weaker antecedent than elabgf 2737. (Contributed by NM, 6-Sep-2011.)
𝑥𝐴    &   𝑥𝜓    &   (𝑥 = 𝐴 → (𝜑𝜓))       ((𝜓𝐴𝐵) → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))

Theoremelab3g 2745* Membership in a class abstraction, with a weaker antecedent than elabg 2740. (Contributed by NM, 29-Aug-2006.)
(𝑥 = 𝐴 → (𝜑𝜓))       ((𝜓𝐴𝐵) → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))

Theoremelab3 2746* Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.)
(𝜓𝐴 ∈ V)    &   (𝑥 = 𝐴 → (𝜑𝜓))       (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)

Theoremelrabi 2747* Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.)
(𝐴 ∈ {𝑥𝑉𝜑} → 𝐴𝑉)

Theoremelrabf 2748 Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.)
𝑥𝐴    &   𝑥𝐵    &   𝑥𝜓    &   (𝑥 = 𝐴 → (𝜑𝜓))       (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))

Theoremelrab3t 2749* Membership in a restricted class abstraction, using implicit substitution. (Closed theorem version of elrab3 2751.) (Contributed by Thierry Arnoux, 31-Aug-2017.)
((∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ 𝐴𝐵) → (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝜓))

Theoremelrab 2750* Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.)
(𝑥 = 𝐴 → (𝜑𝜓))       (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))

Theoremelrab3 2751* Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006.)
(𝑥 = 𝐴 → (𝜑𝜓))       (𝐴𝐵 → (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝜓))

Theoremelrab2 2752* Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   𝐶 = {𝑥𝐵𝜑}       (𝐴𝐶 ↔ (𝐴𝐵𝜓))

Theoremralab 2753* Universal quantification over a class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
(𝑦 = 𝑥 → (𝜑𝜓))       (∀𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∀𝑥(𝜓𝜒))

Theoremralrab 2754* Universal quantification over a restricted class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
(𝑦 = 𝑥 → (𝜑𝜓))       (∀𝑥 ∈ {𝑦𝐴𝜑}𝜒 ↔ ∀𝑥𝐴 (𝜓𝜒))

Theoremrexab 2755* Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 23-Jan-2014.) (Revised by Mario Carneiro, 3-Sep-2015.)
(𝑦 = 𝑥 → (𝜑𝜓))       (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∃𝑥(𝜓𝜒))

Theoremrexrab 2756* Existential quantification over a class abstraction. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Mario Carneiro, 3-Sep-2015.)
(𝑦 = 𝑥 → (𝜑𝜓))       (∃𝑥 ∈ {𝑦𝐴𝜑}𝜒 ↔ ∃𝑥𝐴 (𝜓𝜒))

Theoremralab2 2757* Universal quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015.)
(𝑥 = 𝑦 → (𝜓𝜒))       (∀𝑥 ∈ {𝑦𝜑}𝜓 ↔ ∀𝑦(𝜑𝜒))

Theoremralrab2 2758* Universal quantification over a restricted class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015.)
(𝑥 = 𝑦 → (𝜓𝜒))       (∀𝑥 ∈ {𝑦𝐴𝜑}𝜓 ↔ ∀𝑦𝐴 (𝜑𝜒))

Theoremrexab2 2759* Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015.)
(𝑥 = 𝑦 → (𝜓𝜒))       (∃𝑥 ∈ {𝑦𝜑}𝜓 ↔ ∃𝑦(𝜑𝜒))

Theoremrexrab2 2760* Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015.)
(𝑥 = 𝑦 → (𝜓𝜒))       (∃𝑥 ∈ {𝑦𝐴𝜑}𝜓 ↔ ∃𝑦𝐴 (𝜑𝜒))

Theoremabidnf 2761* Identity used to create closed-form versions of bound-variable hypothesis builders for class expressions. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Mario Carneiro, 12-Oct-2016.)
(𝑥𝐴 → {𝑧 ∣ ∀𝑥 𝑧𝐴} = 𝐴)

Theoremdedhb 2762* A deduction theorem for converting the inference 𝑥𝐴 => 𝜑 into a closed theorem. Use nfa1 1475 and nfab 2224 to eliminate the hypothesis of the substitution instance 𝜓 of the inference. For converting the inference form into a deduction form, abidnf 2761 is useful. (Contributed by NM, 8-Dec-2006.)
(𝐴 = {𝑧 ∣ ∀𝑥 𝑧𝐴} → (𝜑𝜓))    &   𝜓       (𝑥𝐴𝜑)

Theoremeqeu 2763* A condition which implies existential uniqueness. (Contributed by Jeff Hankins, 8-Sep-2009.)
(𝑥 = 𝐴 → (𝜑𝜓))       ((𝐴𝐵𝜓 ∧ ∀𝑥(𝜑𝑥 = 𝐴)) → ∃!𝑥𝜑)

Theoremeueq 2764* Equality has existential uniqueness. (Contributed by NM, 25-Nov-1994.)
(𝐴 ∈ V ↔ ∃!𝑥 𝑥 = 𝐴)

Theoremeueq1 2765* Equality has existential uniqueness. (Contributed by NM, 5-Apr-1995.)
𝐴 ∈ V       ∃!𝑥 𝑥 = 𝐴

Theoremeueq2dc 2766* Equality has existential uniqueness (split into 2 cases). (Contributed by NM, 5-Apr-1995.)
𝐴 ∈ V    &   𝐵 ∈ V       (DECID 𝜑 → ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ 𝜑𝑥 = 𝐵)))

Theoremeueq3dc 2767* Equality has existential uniqueness (split into 3 cases). (Contributed by NM, 5-Apr-1995.) (Proof shortened by Mario Carneiro, 28-Sep-2015.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &    ¬ (𝜑𝜓)       (DECID 𝜑 → (DECID 𝜓 → ∃!𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))

Theoremmoeq 2768* There is at most one set equal to a class. (Contributed by NM, 8-Mar-1995.)
∃*𝑥 𝑥 = 𝐴

Theoremmoeq3dc 2769* "At most one" property of equality (split into 3 cases). (Contributed by Jim Kingdon, 7-Jul-2018.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &    ¬ (𝜑𝜓)       (DECID 𝜑 → (DECID 𝜓 → ∃*𝑥((𝜑𝑥 = 𝐴) ∨ (¬ (𝜑𝜓) ∧ 𝑥 = 𝐵) ∨ (𝜓𝑥 = 𝐶))))

Theoremmosubt 2770* "At most one" remains true after substitution. (Contributed by Jim Kingdon, 18-Jan-2019.)
(∀𝑦∃*𝑥𝜑 → ∃*𝑥𝑦(𝑦 = 𝐴𝜑))

Theoremmosub 2771* "At most one" remains true after substitution. (Contributed by NM, 9-Mar-1995.)
∃*𝑥𝜑       ∃*𝑥𝑦(𝑦 = 𝐴𝜑)

Theoremmo2icl 2772* Theorem for inferring "at most one." (Contributed by NM, 17-Oct-1996.)
(∀𝑥(𝜑𝑥 = 𝐴) → ∃*𝑥𝜑)

Theoremmob2 2773* Consequence of "at most one." (Contributed by NM, 2-Jan-2015.)
(𝑥 = 𝐴 → (𝜑𝜓))       ((𝐴𝐵 ∧ ∃*𝑥𝜑𝜑) → (𝑥 = 𝐴𝜓))

Theoremmoi2 2774* Consequence of "at most one." (Contributed by NM, 29-Jun-2008.)
(𝑥 = 𝐴 → (𝜑𝜓))       (((𝐴𝐵 ∧ ∃*𝑥𝜑) ∧ (𝜑𝜓)) → 𝑥 = 𝐴)

Theoremmob 2775* Equality implied by "at most one." (Contributed by NM, 18-Feb-2006.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑥 = 𝐵 → (𝜑𝜒))       (((𝐴𝐶𝐵𝐷) ∧ ∃*𝑥𝜑𝜓) → (𝐴 = 𝐵𝜒))

Theoremmoi 2776* Equality implied by "at most one." (Contributed by NM, 18-Feb-2006.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑥 = 𝐵 → (𝜑𝜒))       (((𝐴𝐶𝐵𝐷) ∧ ∃*𝑥𝜑 ∧ (𝜓𝜒)) → 𝐴 = 𝐵)

Theoremmorex 2777* Derive membership from uniqueness. (Contributed by Jeff Madsen, 2-Sep-2009.)
𝐵 ∈ V    &   (𝑥 = 𝐵 → (𝜑𝜓))       ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝜑) → (𝜓𝐵𝐴))

Theoremeuxfr2dc 2778* Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 14-Nov-2004.)
𝐴 ∈ V    &   ∃*𝑦 𝑥 = 𝐴       (DECID𝑦𝑥(𝑥 = 𝐴𝜑) → (∃!𝑥𝑦(𝑥 = 𝐴𝜑) ↔ ∃!𝑦𝜑))

Theoremeuxfrdc 2779* Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 14-Nov-2004.)
𝐴 ∈ V    &   ∃!𝑦 𝑥 = 𝐴    &   (𝑥 = 𝐴 → (𝜑𝜓))       (DECID𝑦𝑥(𝑥 = 𝐴𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑦𝜓))

Theoremeuind 2780* Existential uniqueness via an indirect equality. (Contributed by NM, 11-Oct-2010.)
𝐵 ∈ V    &   (𝑥 = 𝑦 → (𝜑𝜓))    &   (𝑥 = 𝑦𝐴 = 𝐵)       ((∀𝑥𝑦((𝜑𝜓) → 𝐴 = 𝐵) ∧ ∃𝑥𝜑) → ∃!𝑧𝑥(𝜑𝑧 = 𝐴))

Theoremreu2 2781* A way to express restricted uniqueness. (Contributed by NM, 22-Nov-1994.)
(∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))

Theoremreu6 2782* A way to express restricted uniqueness. (Contributed by NM, 20-Oct-2006.)
(∃!𝑥𝐴 𝜑 ↔ ∃𝑦𝐴𝑥𝐴 (𝜑𝑥 = 𝑦))

Theoremreu3 2783* A way to express restricted uniqueness. (Contributed by NM, 24-Oct-2006.)
(∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃𝑦𝐴𝑥𝐴 (𝜑𝑥 = 𝑦)))

Theoremreu6i 2784* A condition which implies existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.)
((𝐵𝐴 ∧ ∀𝑥𝐴 (𝜑𝑥 = 𝐵)) → ∃!𝑥𝐴 𝜑)

Theoremeqreu 2785* A condition which implies existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.)
(𝑥 = 𝐵 → (𝜑𝜓))       ((𝐵𝐴𝜓 ∧ ∀𝑥𝐴 (𝜑𝑥 = 𝐵)) → ∃!𝑥𝐴 𝜑)

Theoremrmo4 2786* Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by NM, 16-Jun-2017.)
(𝑥 = 𝑦 → (𝜑𝜓))       (∃*𝑥𝐴 𝜑 ↔ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦))

Theoremreu4 2787* Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994.)
(𝑥 = 𝑦 → (𝜑𝜓))       (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))

Theoremreu7 2788* Restricted uniqueness using implicit substitution. (Contributed by NM, 24-Oct-2006.)
(𝑥 = 𝑦 → (𝜑𝜓))       (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃𝑥𝐴𝑦𝐴 (𝜓𝑥 = 𝑦)))

Theoremreu8 2789* Restricted uniqueness using implicit substitution. (Contributed by NM, 24-Oct-2006.)
(𝑥 = 𝑦 → (𝜑𝜓))       (∃!𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 (𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦)))

Theoremreueq 2790* Equality has existential uniqueness. (Contributed by Mario Carneiro, 1-Sep-2015.)
(𝐵𝐴 ↔ ∃!𝑥𝐴 𝑥 = 𝐵)

Theoremrmoan 2791 Restricted "at most one" still holds when a conjunct is added. (Contributed by NM, 16-Jun-2017.)
(∃*𝑥𝐴 𝜑 → ∃*𝑥𝐴 (𝜓𝜑))

Theoremrmoim 2792 Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.)
(∀𝑥𝐴 (𝜑𝜓) → (∃*𝑥𝐴 𝜓 → ∃*𝑥𝐴 𝜑))

Theoremrmoimia 2793 Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.)
(𝑥𝐴 → (𝜑𝜓))       (∃*𝑥𝐴 𝜓 → ∃*𝑥𝐴 𝜑)

Theoremrmoimi2 2794 Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.)
𝑥((𝑥𝐴𝜑) → (𝑥𝐵𝜓))       (∃*𝑥𝐵 𝜓 → ∃*𝑥𝐴 𝜑)

Theorem2reuswapdc 2795* A condition allowing swap of uniqueness and existential quantifiers. (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by NM, 16-Jun-2017.)
(DECID𝑥𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)) → (∀𝑥𝐴 ∃*𝑦𝐵 𝜑 → (∃!𝑥𝐴𝑦𝐵 𝜑 → ∃!𝑦𝐵𝑥𝐴 𝜑)))

Theoremreuind 2796* Existential uniqueness via an indirect equality. (Contributed by NM, 16-Oct-2010.)
(𝑥 = 𝑦 → (𝜑𝜓))    &   (𝑥 = 𝑦𝐴 = 𝐵)       ((∀𝑥𝑦(((𝐴𝐶𝜑) ∧ (𝐵𝐶𝜓)) → 𝐴 = 𝐵) ∧ ∃𝑥(𝐴𝐶𝜑)) → ∃!𝑧𝐶𝑥((𝐴𝐶𝜑) → 𝑧 = 𝐴))

Theorem2rmorex 2797* Double restricted quantification with "at most one," analogous to 2moex 2028. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
(∃*𝑥𝐴𝑦𝐵 𝜑 → ∀𝑦𝐵 ∃*𝑥𝐴 𝜑)

Theoremnelrdva 2798* Deduce negative membership from an implication. (Contributed by Thierry Arnoux, 27-Nov-2017.)
((𝜑𝑥𝐴) → 𝑥𝐵)       (𝜑 → ¬ 𝐵𝐴)

2.1.7  Conditional equality (experimental)

This is a very useless definition, which "abbreviates" (𝑥 = 𝑦𝜑) as CondEq(𝑥 = 𝑦𝜑). What this display hides, though, is that the first expression, even though it has a shorter constant string, is actually much more complicated in its parse tree: it is parsed as (wi (wceq (cv vx) (cv vy)) wph), while the CondEq version is parsed as (wcdeq vx vy wph). It also allows us to give a name to the specific ternary operation (𝑥 = 𝑦𝜑).

This is all used as part of a metatheorem: we want to say that (𝑥 = 𝑦 → (𝜑(𝑥) ↔ 𝜑(𝑦))) and (𝑥 = 𝑦𝐴(𝑥) = 𝐴(𝑦)) are provable, for any expressions 𝜑(𝑥) or 𝐴(𝑥) in the language. The proof is by induction, so the base case is each of the primitives, which is why you will see a theorem for each of the set.mm primitive operations.

The metatheorem comes with a disjoint variables assumption: every variable in 𝜑(𝑥) is assumed disjoint from 𝑥 except 𝑥 itself. For such a proof by induction, we must consider each of the possible forms of 𝜑(𝑥). If it is a variable other than 𝑥, then we have CondEq(𝑥 = 𝑦𝐴 = 𝐴) or CondEq(𝑥 = 𝑦 → (𝜑𝜑)), which is provable by cdeqth 2803 and reflexivity. Since we are only working with class and wff expressions, it can't be 𝑥 itself in set.mm, but if it was we'd have to also prove CondEq(𝑥 = 𝑦𝑥 = 𝑦) (where set equality is being used on the right).

Otherwise, it is a primitive operation applied to smaller expressions. In these cases, for each setvar variable parameter to the operation, we must consider if it is equal to 𝑥 or not, which yields 2^n proof obligations. Luckily, all primitive operations in set.mm have either zero or one set variable, so we only need to prove one statement for the non-set constructors (like implication) and two for the constructors taking a set (the forall and the class builder).

In each of the primitive proofs, we are allowed to assume that 𝑦 is disjoint from 𝜑(𝑥) and vice versa, because this is maintained through the induction. This is how we satisfy the DV assumptions of cdeqab1 2808 and cdeqab 2806.

Syntaxwcdeq 2799 Extend wff notation to include conditional equality. This is a technical device used in the proof that is the not-free predicate, and that definitions are conservative as a result.
wff CondEq(𝑥 = 𝑦𝜑)

Definitiondf-cdeq 2800 Define conditional equality. All the notation to the left of the is fake; the parentheses and arrows are all part of the notation, which could equally well be written CondEq𝑥𝑦𝜑. On the right side is the actual implication arrow. The reason for this definition is to "flatten" the structure on the right side (whose tree structure is something like (wi (wceq (cv vx) (cv vy)) wph) ) into just (wcdeq vx vy wph). (Contributed by Mario Carneiro, 11-Aug-2016.)
(CondEq(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦𝜑))

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-10953
 Copyright terms: Public domain < Previous  Next >