 Home Intuitionistic Logic ExplorerTheorem List (p. 57 of 114) < 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 - 5601-5700   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremeusvobj2 5601* Specify the same property in two ways when class 𝐵(𝑦) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
𝐵 ∈ V       (∃!𝑥𝑦𝐴 𝑥 = 𝐵 → (∃𝑦𝐴 𝑥 = 𝐵 ↔ ∀𝑦𝐴 𝑥 = 𝐵))

Theoremeusvobj1 5602* Specify the same object in two ways when class 𝐵(𝑦) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
𝐵 ∈ V       (∃!𝑥𝑦𝐴 𝑥 = 𝐵 → (℩𝑥𝑦𝐴 𝑥 = 𝐵) = (℩𝑥𝑦𝐴 𝑥 = 𝐵))

Theoremf1ofveu 5603* There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.)
((𝐹:𝐴1-1-onto𝐵𝐶𝐵) → ∃!𝑥𝐴 (𝐹𝑥) = 𝐶)

Theoremf1ocnvfv3 5604* Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
((𝐹:𝐴1-1-onto𝐵𝐶𝐵) → (𝐹𝐶) = (𝑥𝐴 (𝐹𝑥) = 𝐶))

Theoremriotaund 5605* Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 13-Sep-2018.)
(¬ ∃!𝑥𝐴 𝜑 → (𝑥𝐴 𝜑) = ∅)

Theoremacexmidlema 5606* Lemma for acexmid 5614. (Contributed by Jim Kingdon, 6-Aug-2019.)
𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   𝐶 = {𝐴, 𝐵}       ({∅} ∈ 𝐴𝜑)

Theoremacexmidlemb 5607* Lemma for acexmid 5614. (Contributed by Jim Kingdon, 6-Aug-2019.)
𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   𝐶 = {𝐴, 𝐵}       (∅ ∈ 𝐵𝜑)

Theoremacexmidlemph 5608* Lemma for acexmid 5614. (Contributed by Jim Kingdon, 6-Aug-2019.)
𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   𝐶 = {𝐴, 𝐵}       (𝜑𝐴 = 𝐵)

Theoremacexmidlemab 5609* Lemma for acexmid 5614. (Contributed by Jim Kingdon, 6-Aug-2019.)
𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   𝐶 = {𝐴, 𝐵}       (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}) → ¬ 𝜑)

Theoremacexmidlemcase 5610* Lemma for acexmid 5614. Here we divide the proof into cases (based on the disjunction implicit in an unordered pair, not the sort of case elimination which relies on excluded middle).

The cases are (1) the choice function evaluated at 𝐴 equals {∅}, (2) the choice function evaluated at 𝐵 equals , and (3) the choice function evaluated at 𝐴 equals and the choice function evaluated at 𝐵 equals {∅}.

Because of the way we represent the choice function 𝑦, the choice function evaluated at 𝐴 is (𝑣𝐴𝑢𝑦(𝐴𝑢𝑣𝑢)) and the choice function evaluated at 𝐵 is (𝑣𝐵𝑢𝑦(𝐵𝑢𝑣𝑢)). Other than the difference in notation these work just as (𝑦𝐴) and (𝑦𝐵) would if 𝑦 were a function as defined by df-fun 4985.

Although it isn't exactly about the division into cases, it is also convenient for this lemma to also include the step that if the choice function evaluated at 𝐴 equals {∅}, then {∅} ∈ 𝐴 and likewise for 𝐵.

(Contributed by Jim Kingdon, 7-Aug-2019.)

𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   𝐶 = {𝐴, 𝐵}       (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ({∅} ∈ 𝐴 ∨ ∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})))

Theoremacexmidlem1 5611* Lemma for acexmid 5614. List the cases identified in acexmidlemcase 5610 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.)
𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   𝐶 = {𝐴, 𝐵}       (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (𝜑 ∨ ¬ 𝜑))

Theoremacexmidlem2 5612* Lemma for acexmid 5614. This builds on acexmidlem1 5611 by noting that every element of 𝐶 is inhabited.

(Note that 𝑦 is not quite a function in the df-fun 4985 sense because it uses ordered pairs as described in opthreg 4347 rather than df-op 3440).

The set 𝐴 is also found in onsucelsucexmidlem 4320.

(Contributed by Jim Kingdon, 5-Aug-2019.)

𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   𝐶 = {𝐴, 𝐵}       (∀𝑧𝐶𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (𝜑 ∨ ¬ 𝜑))

Theoremacexmidlemv 5613* Lemma for acexmid 5614.

This is acexmid 5614 with additional distinct variable constraints, most notably between 𝜑 and 𝑥.

(Contributed by Jim Kingdon, 6-Aug-2019.)

𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)       (𝜑 ∨ ¬ 𝜑)

Theoremacexmid 5614* The axiom of choice implies excluded middle. Theorem 1.3 in [Bauer] p. 483.

The statement of the axiom of choice given here is ac2 in the Metamath Proof Explorer (version of 3-Aug-2019). In particular, note that the choice function 𝑦 provides a value when 𝑧 is inhabited (as opposed to nonempty as in some statements of the axiom of choice).

Essentially the same proof can also be found at "The axiom of choice implies instances of EM", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic".

Often referred to as Diaconescu's theorem, or Diaconescu-Goodman-Myhill theorem, after Radu Diaconescu who discovered it in 1975 in the framework of topos theory and N. D. Goodman and John Myhill in 1978 in the framework of set theory (although it already appeared as an exercise in Errett Bishop's book Foundations of Constructive Analysis from 1967).

(Contributed by Jim Kingdon, 4-Aug-2019.)

𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)       (𝜑 ∨ ¬ 𝜑)

2.6.10  Operations

Syntaxco 5615 Extend class notation to include the value of an operation 𝐹 (such as + ) for two arguments 𝐴 and 𝐵. Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous.
class (𝐴𝐹𝐵)

Syntaxcoprab 5616 Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}

Syntaxcmpt2 5617 Extend the definition of a class to include maps-to notation for defining an operation via a rule.
class (𝑥𝐴, 𝑦𝐵𝐶)

Definitiondf-ov 5618 Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. For example, if class 𝐹 is the operation + and arguments 𝐴 and 𝐵 are 3 and 2 , the expression ( 3 + 2 ) can be proved to equal 5 . This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 5644 and ovprc2 5645. On the other hand, we often find uses for this definition when 𝐹 is a proper class. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5619. (Contributed by NM, 28-Feb-1995.)
(𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

Definitiondf-oprab 5619* Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally 𝑥, 𝑦, and 𝑧 are distinct, although the definition doesn't strictly require it. See df-ov 5618 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ovmpt2 5739. (Contributed by NM, 12-Mar-1995.)
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}

Definitiondf-mpt2 5620* Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from 𝑥, 𝑦 (in 𝐴 × 𝐵) to 𝐵(𝑥, 𝑦)." An extension of df-mpt 3878 for two arguments. (Contributed by NM, 17-Feb-2008.)
(𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}

Theoremoveq 5621 Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
(𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))

Theoremoveq1 5622 Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
(𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Theoremoveq2 5623 Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
(𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Theoremoveq12 5624 Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Theoremoveq1i 5625 Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
𝐴 = 𝐵       (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

Theoremoveq2i 5626 Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
𝐴 = 𝐵       (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Theoremoveq12i 5627 Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
𝐴 = 𝐵    &   𝐶 = 𝐷       (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

Theoremoveqi 5628 Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
𝐴 = 𝐵       (𝐶𝐴𝐷) = (𝐶𝐵𝐷)

Theoremoveq123i 5629 Equality inference for operation value. (Contributed by FL, 11-Jul-2010.)
𝐴 = 𝐶    &   𝐵 = 𝐷    &   𝐹 = 𝐺       (𝐴𝐹𝐵) = (𝐶𝐺𝐷)

Theoremoveq1d 5630 Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Theoremoveq2d 5631 Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Theoremoveqd 5632 Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Theoremoveq12d 5633 Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Theoremoveqan12d 5634 Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐶 = 𝐷)       ((𝜑𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Theoremoveqan12rd 5635 Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐶 = 𝐷)       ((𝜓𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Theoremoveq123d 5636 Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)
(𝜑𝐹 = 𝐺)    &   (𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷))

Theoremnfovd 5637 Deduction version of bound-variable hypothesis builder nfov 5638. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
(𝜑𝑥𝐴)    &   (𝜑𝑥𝐹)    &   (𝜑𝑥𝐵)       (𝜑𝑥(𝐴𝐹𝐵))

Theoremnfov 5638 Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)
𝑥𝐴    &   𝑥𝐹    &   𝑥𝐵       𝑥(𝐴𝐹𝐵)

Theoremoprabidlem 5639* Slight elaboration of exdistrfor 1725. A lemma for oprabid 5640. (Contributed by Jim Kingdon, 15-Jan-2019.)
(∃𝑥𝑦(𝑥 = 𝑧𝜓) → ∃𝑥(𝑥 = 𝑧 ∧ ∃𝑦𝜓))

Theoremoprabid 5640 The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Although this theorem would be useful with a distinct variable constraint between 𝑥, 𝑦, and 𝑧, we use ax-bndl 1442 to eliminate that constraint. (Contributed by Mario Carneiro, 20-Mar-2013.)
(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)

Theoremfnovex 5641 The result of an operation is a set. (Contributed by Jim Kingdon, 15-Jan-2019.)
((𝐹 Fn (𝐶 × 𝐷) ∧ 𝐴𝐶𝐵𝐷) → (𝐴𝐹𝐵) ∈ V)

Theoremovexg 5642 Evaluating a set operation at two sets gives a set. (Contributed by Jim Kingdon, 19-Aug-2021.)
((𝐴𝑉𝐹𝑊𝐵𝑋) → (𝐴𝐹𝐵) ∈ V)

Theoremovprc 5643 The value of an operation when the one of the arguments is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by Mario Carneiro, 26-Apr-2015.)
Rel dom 𝐹       (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅)

Theoremovprc1 5644 The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.)
Rel dom 𝐹       𝐴 ∈ V → (𝐴𝐹𝐵) = ∅)

Theoremovprc2 5645 The value of an operation when the second argument is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.)
Rel dom 𝐹       𝐵 ∈ V → (𝐴𝐹𝐵) = ∅)

Theoremcsbov123g 5646 Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
(𝐴𝐷𝐴 / 𝑥(𝐵𝐹𝐶) = (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐹𝐴 / 𝑥𝐶))

Theoremcsbov12g 5647* Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
(𝐴𝑉𝐴 / 𝑥(𝐵𝐹𝐶) = (𝐴 / 𝑥𝐵𝐹𝐴 / 𝑥𝐶))

Theoremcsbov1g 5648* Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
(𝐴𝑉𝐴 / 𝑥(𝐵𝐹𝐶) = (𝐴 / 𝑥𝐵𝐹𝐶))

Theoremcsbov2g 5649* Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
(𝐴𝑉𝐴 / 𝑥(𝐵𝐹𝐶) = (𝐵𝐹𝐴 / 𝑥𝐶))

Theoremrspceov 5650* A frequently used special case of rspc2ev 2728 for operation values. (Contributed by NM, 21-Mar-2007.)
((𝐶𝐴𝐷𝐵𝑆 = (𝐶𝐹𝐷)) → ∃𝑥𝐴𝑦𝐵 𝑆 = (𝑥𝐹𝑦))

Theoremfnotovb 5651 Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5311. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶𝐴𝐷𝐵) → ((𝐶𝐹𝐷) = 𝑅 ↔ ⟨𝐶, 𝐷, 𝑅⟩ ∈ 𝐹))

Theoremopabbrex 5652* A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑓(𝑉𝑊𝐸)𝑝𝜃))    &   ((𝑉 ∈ V ∧ 𝐸 ∈ V) → {⟨𝑓, 𝑝⟩ ∣ 𝜃} ∈ V)       ((𝑉 ∈ V ∧ 𝐸 ∈ V) → {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑉𝑊𝐸)𝑝𝜓)} ∈ V)

Theorem0neqopab 5653 The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.)
¬ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Theorembrabvv 5654* If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Jim Kingdon, 16-Jan-2019.)
(𝑋{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑌 → (𝑋 ∈ V ∧ 𝑌 ∈ V))

Theoremdfoprab2 5655* Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.)
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

Theoremreloprab 5656* An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.)
Rel {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}

Theoremnfoprab1 5657 The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)
𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}

Theoremnfoprab2 5658 The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 30-Jul-2012.)
𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}

Theoremnfoprab3 5659 The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.)
𝑧{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}

Theoremnfoprab 5660* Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.)
𝑤𝜑       𝑤{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}

Theoremoprabbid 5661* Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2014.)
𝑥𝜑    &   𝑦𝜑    &   𝑧𝜑    &   (𝜑 → (𝜓𝜒))       (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜒})

Theoremoprabbidv 5662* Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.)
(𝜑 → (𝜓𝜒))       (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜒})

Theoremoprabbii 5663* Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
(𝜑𝜓)       {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}

Theoremssoprab2 5664 Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 4078. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
(∀𝑥𝑦𝑧(𝜑𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})

Theoremssoprab2b 5665 Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 4079. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥𝑦𝑧(𝜑𝜓))

Theoremeqoprab2b 5666 Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 4082. (Contributed by Mario Carneiro, 4-Jan-2017.)
({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥𝑦𝑧(𝜑𝜓))

Theoremmpt2eq123 5667* An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
((𝐴 = 𝐷 ∧ ∀𝑥𝐴 (𝐵 = 𝐸 ∧ ∀𝑦𝐵 𝐶 = 𝐹)) → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐷, 𝑦𝐸𝐹))

Theoremmpt2eq12 5668* An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
((𝐴 = 𝐶𝐵 = 𝐷) → (𝑥𝐴, 𝑦𝐵𝐸) = (𝑥𝐶, 𝑦𝐷𝐸))

Theoremmpt2eq123dva 5669* An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
(𝜑𝐴 = 𝐷)    &   ((𝜑𝑥𝐴) → 𝐵 = 𝐸)    &   ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶 = 𝐹)       (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐷, 𝑦𝐸𝐹))

Theoremmpt2eq123dv 5670* An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011.)
(𝜑𝐴 = 𝐷)    &   (𝜑𝐵 = 𝐸)    &   (𝜑𝐶 = 𝐹)       (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐷, 𝑦𝐸𝐹))

Theoremmpt2eq123i 5671 An equality inference for the maps-to notation. (Contributed by NM, 15-Jul-2013.)
𝐴 = 𝐷    &   𝐵 = 𝐸    &   𝐶 = 𝐹       (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐷, 𝑦𝐸𝐹)

Theoremmpt2eq3dva 5672* Slightly more general equality inference for the maps-to notation. (Contributed by NM, 17-Oct-2013.)
((𝜑𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)       (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))

Theoremmpt2eq3ia 5673 An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
((𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)       (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷)

Theoremnfmpt21 5674 Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
𝑥(𝑥𝐴, 𝑦𝐵𝐶)

Theoremnfmpt22 5675 Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
𝑦(𝑥𝐴, 𝑦𝐵𝐶)

Theoremnfmpt2 5676* Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
𝑧𝐴    &   𝑧𝐵    &   𝑧𝐶       𝑧(𝑥𝐴, 𝑦𝐵𝐶)

Theoremmpt20 5677 A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
(𝑥 ∈ ∅, 𝑦𝐵𝐶) = ∅

Theoremoprab4 5678* Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)}

Theoremcbvoprab1 5679* Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008.) (Revised by Mario Carneiro, 5-Dec-2016.)
𝑤𝜑    &   𝑥𝜓    &   (𝑥 = 𝑤 → (𝜑𝜓))       {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑤, 𝑦⟩, 𝑧⟩ ∣ 𝜓}

Theoremcbvoprab2 5680* Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)
𝑤𝜑    &   𝑦𝜓    &   (𝑦 = 𝑤 → (𝜑𝜓))       {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑤⟩, 𝑧⟩ ∣ 𝜓}

Theoremcbvoprab12 5681* Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
𝑤𝜑    &   𝑣𝜑    &   𝑥𝜓    &   𝑦𝜓    &   ((𝑥 = 𝑤𝑦 = 𝑣) → (𝜑𝜓))       {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑤, 𝑣⟩, 𝑧⟩ ∣ 𝜓}

Theoremcbvoprab12v 5682* Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.)
((𝑥 = 𝑤𝑦 = 𝑣) → (𝜑𝜓))       {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑤, 𝑣⟩, 𝑧⟩ ∣ 𝜓}

Theoremcbvoprab3 5683* Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)
𝑤𝜑    &   𝑧𝜓    &   (𝑧 = 𝑤 → (𝜑𝜓))       {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ 𝜓}

Theoremcbvoprab3v 5684* Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.) (Revised by David Abernethy, 19-Jun-2012.)
(𝑧 = 𝑤 → (𝜑𝜓))       {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ 𝜓}

Theoremcbvmpt2x 5685* Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 5686 allows 𝐵 to be a function of 𝑥. (Contributed by NM, 29-Dec-2014.)
𝑧𝐵    &   𝑥𝐷    &   𝑧𝐶    &   𝑤𝐶    &   𝑥𝐸    &   𝑦𝐸    &   (𝑥 = 𝑧𝐵 = 𝐷)    &   ((𝑥 = 𝑧𝑦 = 𝑤) → 𝐶 = 𝐸)       (𝑥𝐴, 𝑦𝐵𝐶) = (𝑧𝐴, 𝑤𝐷𝐸)

Theoremcbvmpt2 5686* Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.)
𝑧𝐶    &   𝑤𝐶    &   𝑥𝐷    &   𝑦𝐷    &   ((𝑥 = 𝑧𝑦 = 𝑤) → 𝐶 = 𝐷)       (𝑥𝐴, 𝑦𝐵𝐶) = (𝑧𝐴, 𝑤𝐵𝐷)

Theoremcbvmpt2v 5687* Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 3910, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)
(𝑥 = 𝑧𝐶 = 𝐸)    &   (𝑦 = 𝑤𝐸 = 𝐷)       (𝑥𝐴, 𝑦𝐵𝐶) = (𝑧𝐴, 𝑤𝐵𝐷)

Theoremdmoprab 5688* The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)
dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝜑}

Theoremdmoprabss 5689* The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995.)
dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)

Theoremrnoprab 5690* The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)
ran {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦𝜑}

Theoremrnoprab2 5691* The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.)
ran {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} = {𝑧 ∣ ∃𝑥𝐴𝑦𝐵 𝜑}

Theoremreldmoprab 5692* The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)
Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}

Theoremoprabss 5693* Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ ((V × V) × V)

Theoremeloprabga 5694* The law of concretion for operation class abstraction. Compare elopab 4061. (Contributed by NM, 14-Sep-1999.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.)
((𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶) → (𝜑𝜓))       ((𝐴𝑉𝐵𝑊𝐶𝑋) → (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜓))

Theoremeloprabg 5695* The law of concretion for operation class abstraction. Compare elopab 4061. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑦 = 𝐵 → (𝜓𝜒))    &   (𝑧 = 𝐶 → (𝜒𝜃))       ((𝐴𝑉𝐵𝑊𝐶𝑋) → (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜃))

Theoremssoprab2i 5696* Inference of operation class abstraction subclass from implication. (Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy, 19-Jun-2012.)
(𝜑𝜓)       {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}

Theoremmpt2v 5697* Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
(𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑧 = 𝐶}

Theoremmpt2mptx 5698* Express a two-argument function as a one-argument function, or vice-versa. In this version 𝐵(𝑥) is not assumed to be constant w.r.t 𝑥. (Contributed by Mario Carneiro, 29-Dec-2014.)
(𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)       (𝑧 𝑥𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥𝐴, 𝑦𝐵𝐷)

Theoremmpt2mpt 5699* Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by Mario Carneiro, 29-Dec-2014.)
(𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)       (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥𝐴, 𝑦𝐵𝐷)

Theoremresoprab 5700* Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007.)
({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↾ (𝐴 × 𝐵)) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)}

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-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11394
 Copyright terms: Public domain < Previous  Next >