 Home Intuitionistic Logic ExplorerTheorem List (p. 55 of 74) < 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 - 5401-5500   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremriotacl2 5401 Membership law for "the unique element in A such that φ."

(Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)

(∃!x A φ → (x A φ) {x Aφ})

Theoremriotacl 5402* Closure of restricted iota. (Contributed by NM, 21-Aug-2011.)
(∃!x A φ → (x A φ) A)

Theoremriotasbc 5403 Substitution law for descriptions. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
(∃!x A φ[(x A φ) / x]φ)

Theoremriotabidva 5404* Equivalent wff's yield equal restricted class abstractions (deduction rule). (rabbidva 2522 analog.) (Contributed by NM, 17-Jan-2012.)
((φ x A) → (ψχ))       (φ → (x A ψ) = (x A χ))

Theoremriotabiia 5405 Equivalent wff's yield equal restricted iotas (inference rule). (rabbiia 2521 analog.) (Contributed by NM, 16-Jan-2012.)
(x A → (φψ))       (x A φ) = (x A ψ)

Theoremriota1 5406* Property of restricted iota. Compare iota1 4804. (Contributed by Mario Carneiro, 15-Oct-2016.)
(∃!x A φ → ((x A φ) ↔ (x A φ) = x))

Theoremriota1a 5407 Property of iota. (Contributed by NM, 23-Aug-2011.)
((x A ∃!x A φ) → (φ ↔ (℩x(x A φ)) = x))

Theoremriota2df 5408* A deduction version of riota2f 5409. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
xφ    &   (φxB)    &   (φ → Ⅎxχ)    &   (φB A)    &   ((φ x = B) → (ψχ))       ((φ ∃!x A ψ) → (χ ↔ (x A ψ) = B))

Theoremriota2f 5409* This theorem shows a condition that allows us to represent a descriptor with a class expression B. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
xB    &   xψ    &   (x = B → (φψ))       ((B A ∃!x A φ) → (ψ ↔ (x A φ) = B))

Theoremriota2 5410* This theorem shows a condition that allows us to represent a descriptor with a class expression B. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.)
(x = B → (φψ))       ((B A ∃!x A φ) → (ψ ↔ (x A φ) = B))

Theoremriotaprop 5411* Properties of a restricted definite description operator. Todo (df-riota 5389 update): can some uses of riota2f 5409 be shortened with this? (Contributed by NM, 23-Nov-2013.)
xψ    &   B = (x A φ)    &   (x = B → (φψ))       (∃!x A φ → (B A ψ))

Theoremriota5f 5412* A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
(φxB)    &   (φB A)    &   ((φ x A) → (ψx = B))       (φ → (x A ψ) = B)

Theoremriota5 5413* A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.)
(φB A)    &   ((φ x A) → (ψx = B))       (φ → (x A ψ) = B)

Theoremriotass2 5414* Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.)
(((AB x A (φψ)) (x A φ ∃!x B ψ)) → (x A φ) = (x B ψ))

Theoremriotass 5415* Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.)
((AB x A φ ∃!x B φ) → (x A φ) = (x B φ))

Theoremmoriotass 5416* Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.)
((AB x A φ ∃*x B φ) → (x A φ) = (x B φ))

Theoremsnriota 5417 A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.)
(∃!x A φ → {x Aφ} = {(x A φ)})

Theoremeusvobj2 5418* Specify the same property in two ways when class B(y) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
B V       (∃!xy A x = B → (y A x = By A x = B))

Theoremeusvobj1 5419* Specify the same object in two ways when class B(y) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
B V       (∃!xy A x = B → (℩xy A x = B) = (℩xy A x = B))

Theoremf1ofveu 5420* There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.)
((𝐹:A1-1-ontoB 𝐶 B) → ∃!x A (𝐹x) = 𝐶)

Theoremf1ocnvfv3 5421* 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.)
((𝐹:A1-1-ontoB 𝐶 B) → (𝐹𝐶) = (x A (𝐹x) = 𝐶))

Theoremriotaund 5422* 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.)
∃!x A φ → (x A φ) = ∅)

Theoremacexmidlema 5423* Lemma for acexmid 5431. (Contributed by Jim Kingdon, 6-Aug-2019.)
A = {x {∅, {∅}} ∣ (x = ∅ φ)}    &   B = {x {∅, {∅}} ∣ (x = {∅} φ)}    &   𝐶 = {A, B}       ({∅} Aφ)

Theoremacexmidlemb 5424* Lemma for acexmid 5431. (Contributed by Jim Kingdon, 6-Aug-2019.)
A = {x {∅, {∅}} ∣ (x = ∅ φ)}    &   B = {x {∅, {∅}} ∣ (x = {∅} φ)}    &   𝐶 = {A, B}       (∅ Bφ)

Theoremacexmidlemph 5425* Lemma for acexmid 5431. (Contributed by Jim Kingdon, 6-Aug-2019.)
A = {x {∅, {∅}} ∣ (x = ∅ φ)}    &   B = {x {∅, {∅}} ∣ (x = {∅} φ)}    &   𝐶 = {A, B}       (φA = B)

Theoremacexmidlemab 5426* Lemma for acexmid 5431. (Contributed by Jim Kingdon, 6-Aug-2019.)
A = {x {∅, {∅}} ∣ (x = ∅ φ)}    &   B = {x {∅, {∅}} ∣ (x = {∅} φ)}    &   𝐶 = {A, B}       (((v A u y (A u v u)) = ∅ (v B u y (B u v u)) = {∅}) → ¬ φ)

Theoremacexmidlemcase 5427* Lemma for acexmid 5431. 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 A equals {∅}, (2) the choice function evaluated at B equals , and (3) the choice function evaluated at A equals and the choice function evaluated at B equals {∅}.

Because of the way we represent the choice function y, the choice function evaluated at A is (v Au y(A u v u)) and the choice function evaluated at B is (v Bu y(B u v u)). Other than the difference in notation these work just as (yA) and (yB) would if y were a function as defined by df-fun 4827.

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 A equals {∅}, then {∅} A and likewise for B.

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

A = {x {∅, {∅}} ∣ (x = ∅ φ)}    &   B = {x {∅, {∅}} ∣ (x = {∅} φ)}    &   𝐶 = {A, B}       (z 𝐶 ∃!v z u y (z u v u) → ({∅} A B ((v A u y (A u v u)) = ∅ (v B u y (B u v u)) = {∅})))

Theoremacexmidlem1 5428* Lemma for acexmid 5431. List the cases identified in acexmidlemcase 5427 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.)
A = {x {∅, {∅}} ∣ (x = ∅ φ)}    &   B = {x {∅, {∅}} ∣ (x = {∅} φ)}    &   𝐶 = {A, B}       (z 𝐶 ∃!v z u y (z u v u) → (φ ¬ φ))

Theoremacexmidlem2 5429* Lemma for acexmid 5431. This builds on acexmidlem1 5428 by noting that every element of 𝐶 is inhabited.

(Note that y is not quite a function in the df-fun 4827 sense because it uses ordered pairs as described in opthreg 4214 rather than df-op 3355).

The set A is also found in onsucelsucexmidlem 4194.

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

A = {x {∅, {∅}} ∣ (x = ∅ φ)}    &   B = {x {∅, {∅}} ∣ (x = {∅} φ)}    &   𝐶 = {A, B}       (z 𝐶 w z ∃!v z u y (z u v u) → (φ ¬ φ))

Theoremacexmidlemv 5430* Lemma for acexmid 5431.

This is acexmid 5431 with additional distinct variable constraints, most notably between φ and x.

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

yz x w z ∃!v z u y (z u v u)       (φ ¬ φ)

Theoremacexmid 5431* 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 y provides a value when z is inhabited (as opposed to non-empty 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.)

yz x w z ∃!v z u y (z u v u)       (φ ¬ φ)

2.6.10  Operations

Syntaxco 5432 Extend class notation to include the value of an operation 𝐹 (such as + ) for two arguments A and B. 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 (A𝐹B)

Syntaxcoprab 5433 Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class {⟨⟨x, y⟩, z⟩ ∣ φ}

Syntaxcmpt2 5434 Extend the definition of a class to include maps-to notation for defining an operation via a rule.
class (x A, y B𝐶)

Definitiondf-ov 5435 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 A and B- will be useful for proving meaningful theorems. For example, if class 𝐹 is the operation + and arguments A and B 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 A and/or B are proper classes (i.e. are not sets); see ovprc1 5460 and ovprc2 5461. 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 5436. (Contributed by NM, 28-Feb-1995.)
(A𝐹B) = (𝐹‘⟨A, B⟩)

Definitiondf-oprab 5436* 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 x, y, and z are distinct, although the definition doesn't strictly require it. See df-ov 5435 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 5555. (Contributed by NM, 12-Mar-1995.)
{⟨⟨x, y⟩, z⟩ ∣ φ} = {wxyz(w = ⟨⟨x, y⟩, z φ)}

Definitiondf-mpt2 5437* Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x, y (in A × B) to B(x, y)." An extension of df-mpt 3790 for two arguments. (Contributed by NM, 17-Feb-2008.)
(x A, y B𝐶) = {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) z = 𝐶)}

Theoremoveq 5438 Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
(𝐹 = 𝐺 → (A𝐹B) = (A𝐺B))

Theoremoveq1 5439 Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
(A = B → (A𝐹𝐶) = (B𝐹𝐶))

Theoremoveq2 5440 Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
(A = B → (𝐶𝐹A) = (𝐶𝐹B))

Theoremoveq12 5441 Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
((A = B 𝐶 = 𝐷) → (A𝐹𝐶) = (B𝐹𝐷))

Theoremoveq1i 5442 Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
A = B       (A𝐹𝐶) = (B𝐹𝐶)

Theoremoveq2i 5443 Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
A = B       (𝐶𝐹A) = (𝐶𝐹B)

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

Theoremoveqi 5445 Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
A = B       (𝐶A𝐷) = (𝐶B𝐷)

Theoremoveq123i 5446 Equality inference for operation value. (Contributed by FL, 11-Jul-2010.)
A = 𝐶    &   B = 𝐷    &   𝐹 = 𝐺       (A𝐹B) = (𝐶𝐺𝐷)

Theoremoveq1d 5447 Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
(φA = B)       (φ → (A𝐹𝐶) = (B𝐹𝐶))

Theoremoveq2d 5448 Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
(φA = B)       (φ → (𝐶𝐹A) = (𝐶𝐹B))

Theoremoveqd 5449 Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)
(φA = B)       (φ → (𝐶A𝐷) = (𝐶B𝐷))

Theoremoveq12d 5450 Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
(φA = B)    &   (φ𝐶 = 𝐷)       (φ → (A𝐹𝐶) = (B𝐹𝐷))

Theoremoveqan12d 5451 Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
(φA = B)    &   (ψ𝐶 = 𝐷)       ((φ ψ) → (A𝐹𝐶) = (B𝐹𝐷))

Theoremoveqan12rd 5452 Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
(φA = B)    &   (ψ𝐶 = 𝐷)       ((ψ φ) → (A𝐹𝐶) = (B𝐹𝐷))

Theoremoveq123d 5453 Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)
(φ𝐹 = 𝐺)    &   (φA = B)    &   (φ𝐶 = 𝐷)       (φ → (A𝐹𝐶) = (B𝐺𝐷))

Theoremnfovd 5454 Deduction version of bound-variable hypothesis builder nfov 5455. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
(φxA)    &   (φx𝐹)    &   (φxB)       (φx(A𝐹B))

Theoremnfov 5455 Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)
xA    &   x𝐹    &   xB       x(A𝐹B)

Theoremoprabidlem 5456* Slight elaboration of exdistrfor 1659. A lemma for oprabid 5457. (Contributed by Jim Kingdon, 15-Jan-2019.)
(xy(x = z ψ) → x(x = z yψ))

Theoremoprabid 5457 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 x, y, and z, we use ax-bnd 1376 to eliminate that constraint. (Contributed by Mario Carneiro, 20-Mar-2013.)
(⟨⟨x, y⟩, z {⟨⟨x, y⟩, z⟩ ∣ φ} ↔ φ)

Theoremfnovex 5458 The result of an operation is a set. (Contributed by Jim Kingdon, 15-Jan-2019.)
((𝐹 Fn (𝐶 × 𝐷) A 𝐶 B 𝐷) → (A𝐹B) V)

Theoremovprc 5459 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 𝐹       (¬ (A V B V) → (A𝐹B) = ∅)

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

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

Theoremcsbov123g 5462 Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
(A 𝐷A / x(B𝐹𝐶) = (A / xBA / x𝐹A / x𝐶))

Theoremcsbov12g 5463* Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
(A 𝑉A / x(B𝐹𝐶) = (A / xB𝐹A / x𝐶))

Theoremcsbov1g 5464* Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
(A 𝑉A / x(B𝐹𝐶) = (A / xB𝐹𝐶))

Theoremcsbov2g 5465* Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
(A 𝑉A / x(B𝐹𝐶) = (B𝐹A / x𝐶))

Theoremrspceov 5466* A frequently used special case of rspc2ev 2637 for operation values. (Contributed by NM, 21-Mar-2007.)
((𝐶 A 𝐷 B 𝑆 = (𝐶𝐹𝐷)) → x A y B 𝑆 = (x𝐹y))

Theoremfnotovb 5467 Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5136. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
((𝐹 Fn (A × B) 𝐶 A 𝐷 B) → ((𝐶𝐹𝐷) = 𝑅 ↔ ⟨𝐶, 𝐷, 𝑅 𝐹))

Theoremopabbrex 5468* 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) → (f(𝑉𝑊𝐸)𝑝θ))    &   ((𝑉 V 𝐸 V) → {⟨f, 𝑝⟩ ∣ θ} V)       ((𝑉 V 𝐸 V) → {⟨f, 𝑝⟩ ∣ (f(𝑉𝑊𝐸)𝑝 ψ)} V)

Theorem0neqopab 5469 The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.)
¬ ∅ {⟨x, y⟩ ∣ φ}

Theorembrabvv 5470* 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.)
(𝑋{⟨x, y⟩ ∣ φ}𝑌 → (𝑋 V 𝑌 V))

Theoremdfoprab2 5471* Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.)
{⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨w, z⟩ ∣ xy(w = ⟨x, y φ)}

Theoremreloprab 5472* An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.)
Rel {⟨⟨x, y⟩, z⟩ ∣ φ}

Theoremnfoprab1 5473 The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)
x{⟨⟨x, y⟩, z⟩ ∣ φ}

Theoremnfoprab2 5474 The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 30-Jul-2012.)
y{⟨⟨x, y⟩, z⟩ ∣ φ}

Theoremnfoprab3 5475 The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.)
z{⟨⟨x, y⟩, z⟩ ∣ φ}

Theoremnfoprab 5476* Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.)
wφ       w{⟨⟨x, y⟩, z⟩ ∣ φ}

Theoremoprabbid 5477* Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2014.)
xφ    &   yφ    &   zφ    &   (φ → (ψχ))       (φ → {⟨⟨x, y⟩, z⟩ ∣ ψ} = {⟨⟨x, y⟩, z⟩ ∣ χ})

Theoremoprabbidv 5478* Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.)
(φ → (ψχ))       (φ → {⟨⟨x, y⟩, z⟩ ∣ ψ} = {⟨⟨x, y⟩, z⟩ ∣ χ})

Theoremoprabbii 5479* Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
(φψ)       {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, z⟩ ∣ ψ}

Theoremssoprab2 5480 Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 3982. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
(xyz(φψ) → {⟨⟨x, y⟩, z⟩ ∣ φ} ⊆ {⟨⟨x, y⟩, z⟩ ∣ ψ})

Theoremssoprab2b 5481 Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 3983. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
({⟨⟨x, y⟩, z⟩ ∣ φ} ⊆ {⟨⟨x, y⟩, z⟩ ∣ ψ} ↔ xyz(φψ))

Theoremeqoprab2b 5482 Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 3986. (Contributed by Mario Carneiro, 4-Jan-2017.)
({⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, z⟩ ∣ ψ} ↔ xyz(φψ))

Theoremmpt2eq123 5483* An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
((A = 𝐷 x A (B = 𝐸 y B 𝐶 = 𝐹)) → (x A, y B𝐶) = (x 𝐷, y 𝐸𝐹))

Theoremmpt2eq12 5484* An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
((A = 𝐶 B = 𝐷) → (x A, y B𝐸) = (x 𝐶, y 𝐷𝐸))

Theoremmpt2eq123dva 5485* An equality deduction for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
(φA = 𝐷)    &   ((φ x A) → B = 𝐸)    &   ((φ (x A y B)) → 𝐶 = 𝐹)       (φ → (x A, y B𝐶) = (x 𝐷, y 𝐸𝐹))

Theoremmpt2eq123dv 5486* An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.)
(φA = 𝐷)    &   (φB = 𝐸)    &   (φ𝐶 = 𝐹)       (φ → (x A, y B𝐶) = (x 𝐷, y 𝐸𝐹))

Theoremmpt2eq123i 5487 An equality inference for the maps to notation. (Contributed by NM, 15-Jul-2013.)
A = 𝐷    &   B = 𝐸    &   𝐶 = 𝐹       (x A, y B𝐶) = (x 𝐷, y 𝐸𝐹)

Theoremmpt2eq3dva 5488* Slightly more general equality inference for the maps to notation. (Contributed by NM, 17-Oct-2013.)
((φ x A y B) → 𝐶 = 𝐷)       (φ → (x A, y B𝐶) = (x A, y B𝐷))

Theoremmpt2eq3ia 5489 An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
((x A y B) → 𝐶 = 𝐷)       (x A, y B𝐶) = (x A, y B𝐷)

Theoremnfmpt21 5490 Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
x(x A, y B𝐶)

Theoremnfmpt22 5491 Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
y(x A, y B𝐶)

Theoremnfmpt2 5492* Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
zA    &   zB    &   z𝐶       z(x A, y B𝐶)

Theoremmpt20 5493 A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
(x ∅, y B𝐶) = ∅

Theoremoprab4 5494* Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)
{⟨⟨x, y⟩, z⟩ ∣ (⟨x, y (A × B) φ)} = {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) φ)}

Theoremcbvoprab1 5495* 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.)
wφ    &   xψ    &   (x = w → (φψ))       {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨w, y⟩, z⟩ ∣ ψ}

Theoremcbvoprab2 5496* Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)
wφ    &   yψ    &   (y = w → (φψ))       {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, w⟩, z⟩ ∣ ψ}

Theoremcbvoprab12 5497* 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.)
wφ    &   vφ    &   xψ    &   yψ    &   ((x = w y = v) → (φψ))       {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨w, v⟩, z⟩ ∣ ψ}

Theoremcbvoprab12v 5498* Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.)
((x = w y = v) → (φψ))       {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨w, v⟩, z⟩ ∣ ψ}

Theoremcbvoprab3 5499* Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)
wφ    &   zψ    &   (z = w → (φψ))       {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, w⟩ ∣ ψ}

Theoremcbvoprab3v 5500* 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.)
(z = w → (φψ))       {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, w⟩ ∣ ψ}

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-7354
 Copyright terms: Public domain < Previous  Next >