Home Intuitionistic Logic ExplorerTheorem List (p. 40 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

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

Theoremelpw2g 3901 Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)
(B 𝑉 → (A 𝒫 BAB))

Theoremelpw2 3902 Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
B V       (A 𝒫 BAB)

Theorempwnss 3903 The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.)
(A 𝑉 → ¬ 𝒫 AA)

Theorempwne 3904 No set equals its power set. The sethood antecedent is necessary; compare pwv 3570. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
(A 𝑉 → 𝒫 AA)

Theoremrepizf2lem 3905 Lemma for repizf2 3906. If we have a function-like proposition which provides at most one value of y for each x in a set w, we can change "at most one" to "exactly one" by restricting the values of x to those values for which the proposition provides a value of y. (Contributed by Jim Kingdon, 7-Sep-2018.)
(x w ∃*yφx {x wyφ}∃!yφ)

Theoremrepizf2 3906* Replacement. This version of replacement is stronger than repizf 3864 in the sense that φ does not need to map all values of x in w to a value of y. The resulting set contains those elements for which there is a value of y and in that sense, this theorem combines repizf 3864 with ax-sep 3866. Another variation would be x w∃*yφ → {yx(x w φ)} V but we don't have a proof of that yet. (Contributed by Jim Kingdon, 7-Sep-2018.)
zφ       (x w ∃*yφzx {x wyφ}y z φ)

2.2.5  Theorems requiring empty set existence

Theoremclass2seteq 3907* Equality theorem for classes and sets . (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.)
(A 𝑉 → {x AA V} = A)

Theorem0elpw 3908 Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.)
𝒫 A

Theorem0nep0 3909 The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.)
∅ ≠ {∅}

Theorem0inp0 3910 Something cannot be equal to both the null set and the power set of the null set. (Contributed by NM, 30-Sep-2003.)
(A = ∅ → ¬ A = {∅})

Theoremunidif0 3911 The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.)
(A ∖ {∅}) = A

Theoremiin0imm 3912* An indexed intersection of the empty set, with an inhabited index set, is empty. (Contributed by Jim Kingdon, 29-Aug-2018.)
(y y A x A ∅ = ∅)

Theoremiin0r 3913* If an indexed intersection of the empty set is empty, the index set is non-empty. (Contributed by Jim Kingdon, 29-Aug-2018.)
( x A ∅ = ∅ → A ≠ ∅)

Theoremintv 3914 The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.)
V = ∅

Theoremaxpweq 3915* Two equivalent ways to express the Power Set Axiom. Note that ax-pow 3918 is not used by the proof. (Contributed by NM, 22-Jun-2009.)
A V       (𝒫 A V ↔ xy(z(z yz A) → y x))

2.2.6  Collection principle

Theorembnd 3916* A very strong generalization of the Axiom of Replacement (compare zfrep6 3865). Its strength lies in the rather profound fact that φ(x, y) does not have to be a "function-like" wff, as it does in the standard Axiom of Replacement. This theorem is sometimes called the Boundedness Axiom. In the context of IZF, it is just a slight variation of ax-coll 3863. (Contributed by NM, 17-Oct-2004.)
(x z yφwx z y w φ)

Theorembnd2 3917* A variant of the Boundedness Axiom bnd 3916 that picks a subset z out of a possibly proper class B in which a property is true. (Contributed by NM, 4-Feb-2004.)
A V       (x A y B φz(zB x A y z φ))

2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing

2.3.1  Introduce the Axiom of Power Sets

Axiomax-pow 3918* Axiom of Power Sets. An axiom of Intuitionistic Zermelo-Fraenkel set theory. It states that a set y exists that includes the power set of a given set x i.e. contains every subset of x. This is Axiom 8 of [Crosilla] p. "Axioms of CZF and IZF" except (a) unnecessary quantifiers are removed, and (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 3869).

The variant axpow2 3920 uses explicit subset notation. A version using class notation is pwex 3923. (Contributed by NM, 5-Aug-1993.)

yz(w(w zw x) → z y)

Theoremzfpow 3919* Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.)
xy(x(x yx z) → y x)

Theoremaxpow2 3920* A variant of the Axiom of Power Sets ax-pow 3918 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
yz(zxz y)

Theoremaxpow3 3921* A variant of the Axiom of Power Sets ax-pow 3918. For any set x, there exists a set y whose members are exactly the subsets of x i.e. the power set of x. Axiom Pow of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
yz(zxz y)

Theoremel 3922* Every set is an element of some other set. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
y x y

Theorempwex 3923 Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
A V       𝒫 A V

Theorempwexg 3924 Power set axiom expressed in class notation, with the sethood requirement as an antecedent. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.)
(A 𝑉 → 𝒫 A V)

Theoremabssexg 3925* Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(A 𝑉 → {x ∣ (xA φ)} V)

TheoremsnexgOLD 3926 A singleton whose element exists is a set. The A V case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. This is a special case of snexg 3927 and new proofs should use snexg 3927 instead. (Contributed by Jim Kingdon, 26-Jan-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of snexg 3927 and then remove it.
(A V → {A} V)

Theoremsnexg 3927 A singleton whose element exists is a set. The A V case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.)
(A 𝑉 → {A} V)

Theoremsnex 3928 A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)
A V       {A} V

Theoremsnexprc 3929 A singleton whose element is a proper class is a set. The ¬ A V case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.)
A V → {A} V)

Theoremp0ex 3930 The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.)
{∅} V

Theorempp0ex 3931 {∅, {∅}} (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.)
{∅, {∅}} V

Theoremord3ex 3932 The ordinal number 3 is a set, proved without the Axiom of Union. (Contributed by NM, 2-May-2009.)
{∅, {∅}, {∅, {∅}}} V

Theoremdtruarb 3933* At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). This theorem asserts the existence of two sets which do not equal each other; compare with dtruex 4237 in which we are given a set y and go from there to a set x which is not equal to it. (Contributed by Jim Kingdon, 2-Sep-2018.)
xy ¬ x = y

Theorempwuni 3934 A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.)
A ⊆ 𝒫 A

2.3.2  Axiom of Pairing

Axiomax-pr 3935* The Axiom of Pairing of IZF set theory. Axiom 2 of [Crosilla] p. "Axioms of CZF and IZF", except (a) unnecessary quantifiers are removed, and (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 3869). (Contributed by NM, 14-Nov-2006.)
zw((w = x w = y) → w z)

Theoremzfpair2 3936 Derive the abbreviated version of the Axiom of Pairing from ax-pr 3935. (Contributed by NM, 14-Nov-2006.)
{x, y} V

TheoremprexgOLD 3937 The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51, but restricted to classes which exist. For proper classes, see prprc 3471, prprc1 3469, and prprc2 3470. This is a special case of prexg 3938 and new proofs should use prexg 3938 instead. (Contributed by Jim Kingdon, 25-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of prexg 3938 and then remove it.
((A V B V) → {A, B} V)

Theoremprexg 3938 The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51, but restricted to classes which exist. For proper classes, see prprc 3471, prprc1 3469, and prprc2 3470. (Contributed by Jim Kingdon, 16-Sep-2018.)
((A 𝑉 B 𝑊) → {A, B} V)

Theoremsnelpwi 3939 A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.)
(A B → {A} 𝒫 B)

Theoremsnelpw 3940 A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.)
A V       (A B ↔ {A} 𝒫 B)

Theoremprelpwi 3941 A pair of two sets belongs to the power class of a class containing those two sets. (Contributed by Thierry Arnoux, 10-Mar-2017.)
((A 𝐶 B 𝐶) → {A, B} 𝒫 𝐶)

Theoremrext 3942* A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of [TakeutiZaring] p. 16. (Contributed by NM, 10-Aug-1993.)
(z(x zy z) → x = y)

Theoremsspwb 3943 Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.)
(AB ↔ 𝒫 A ⊆ 𝒫 B)

Theoremunipw 3944 A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) (Proof shortened by Alan Sare, 28-Dec-2008.)
𝒫 A = A

Theorempwel 3945 Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.)
(A B → 𝒫 A 𝒫 𝒫 B)

Theorempwtr 3946 A class is transitive iff its power class is transitive. (Contributed by Alan Sare, 25-Aug-2011.) (Revised by Mario Carneiro, 15-Jun-2014.)
(Tr A ↔ Tr 𝒫 A)

Theoremssextss 3947* An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.)
(ABx(xAxB))

Theoremssext 3948* An extensionality-like principle that uses the subset instead of the membership relation: two classes are equal iff they have the same subsets. (Contributed by NM, 30-Jun-2004.)
(A = Bx(xAxB))

Theoremnssssr 3949* Negation of subclass relationship. Compare nssr 2997. (Contributed by Jim Kingdon, 17-Sep-2018.)
(x(xA ¬ xB) → ¬ AB)

Theorempweqb 3950 Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.)
(A = B ↔ 𝒫 A = 𝒫 B)

Theoremintid 3951* The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.)
A V        {xA x} = {A}

Theoremeuabex 3952 The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.)
(∃!xφ → {xφ} V)

Theoremmss 3953* An inhabited class (even if proper) has an inhabited subset. (Contributed by Jim Kingdon, 17-Sep-2018.)
(y y Ax(xA z z x))

Theoremexss 3954* Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.)
(x A φy(yA x y φ))

Theoremopexg 3955 An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.)
((A 𝑉 B 𝑊) → ⟨A, B V)

TheoremopexgOLD 3956 An ordered pair of sets is a set. This is a special case of opexg 3955 and new proofs should use opexg 3955 instead. (Contributed by Jim Kingdon, 19-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of opexg 3955 and then remove it.
((A V B V) → ⟨A, B V)

Theoremopex 3957 An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.)
A V    &   B V       A, B V

Theoremotexg 3958 An ordered triple of sets is a set. (Contributed by Jim Kingdon, 19-Sep-2018.)
((A 𝑈 B 𝑉 𝐶 𝑊) → ⟨A, B, 𝐶 V)

Theoremelop 3959 An ordered pair has two elements. Exercise 3 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
A V    &   B V    &   𝐶 V       (A B, 𝐶⟩ ↔ (A = {B} A = {B, 𝐶}))

Theoremopi1 3960 One of the two elements in an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
A V    &   B V       {A} A, B

Theoremopi2 3961 One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
A V    &   B V       {A, B} A, B

2.3.3  Ordered pair theorem

Theoremopm 3962* An ordered pair is inhabited iff the arguments are sets. (Contributed by Jim Kingdon, 21-Sep-2018.)
(x x A, B⟩ ↔ (A V B V))

Theoremopnzi 3963 An ordered pair is nonempty if the arguments are sets (it is also inhabited; see opm 3962). (Contributed by Mario Carneiro, 26-Apr-2015.)
A V    &   B V       A, B⟩ ≠ ∅

Theoremopth1 3964 Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
A V    &   B V       (⟨A, B⟩ = ⟨𝐶, 𝐷⟩ → A = 𝐶)

Theoremopth 3965 The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that 𝐶 and 𝐷 are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995.)
A V    &   B V       (⟨A, B⟩ = ⟨𝐶, 𝐷⟩ ↔ (A = 𝐶 B = 𝐷))

Theoremopthg 3966 Ordered pair theorem. 𝐶 and 𝐷 are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.)
((A 𝑉 B 𝑊) → (⟨A, B⟩ = ⟨𝐶, 𝐷⟩ ↔ (A = 𝐶 B = 𝐷)))

Theoremopthg2 3967 Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.)
((𝐶 𝑉 𝐷 𝑊) → (⟨A, B⟩ = ⟨𝐶, 𝐷⟩ ↔ (A = 𝐶 B = 𝐷)))

Theoremopth2 3968 Ordered pair theorem. (Contributed by NM, 21-Sep-2014.)
𝐶 V    &   𝐷 V       (⟨A, B⟩ = ⟨𝐶, 𝐷⟩ ↔ (A = 𝐶 B = 𝐷))

Theoremotth2 3969 Ordered triple theorem, with triple express with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.)
A V    &   B V    &   𝑅 V       (⟨⟨A, B⟩, 𝑅⟩ = ⟨⟨𝐶, 𝐷⟩, 𝑆⟩ ↔ (A = 𝐶 B = 𝐷 𝑅 = 𝑆))

Theoremotth 3970 Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
A V    &   B V    &   𝑅 V       (⟨A, B, 𝑅⟩ = ⟨𝐶, 𝐷, 𝑆⟩ ↔ (A = 𝐶 B = 𝐷 𝑅 = 𝑆))

Theoremeqvinop 3971* A variable introduction law for ordered pairs. Analog of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.)
B V    &   𝐶 V       (A = ⟨B, 𝐶⟩ ↔ xy(A = ⟨x, yx, y⟩ = ⟨B, 𝐶⟩))

Theoremcopsexg 3972* Substitution of class A for ordered pair x, y. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.)
(A = ⟨x, y⟩ → (φxy(A = ⟨x, y φ)))

Theoremcopsex2t 3973* Closed theorem form of copsex2g 3974. (Contributed by NM, 17-Feb-2013.)
((xy((x = A y = B) → (φψ)) (A 𝑉 B 𝑊)) → (xy(⟨A, B⟩ = ⟨x, y φ) ↔ ψ))

Theoremcopsex2g 3974* Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.)
((x = A y = B) → (φψ))       ((A 𝑉 B 𝑊) → (xy(⟨A, B⟩ = ⟨x, y φ) ↔ ψ))

Theoremcopsex4g 3975* An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.)
(((x = A y = B) (z = 𝐶 w = 𝐷)) → (φψ))       (((A 𝑅 B 𝑆) (𝐶 𝑅 𝐷 𝑆)) → (xyzw((⟨A, B⟩ = ⟨x, y𝐶, 𝐷⟩ = ⟨z, w⟩) φ) ↔ ψ))

Theorem0nelop 3976 A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
¬ ∅ A, B

Theoremopeqex 3977 Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.)
(⟨A, B⟩ = ⟨𝐶, 𝐷⟩ → ((A V B V) ↔ (𝐶 V 𝐷 V)))

Theoremopcom 3978 An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.)
A V    &   B V       (⟨A, B⟩ = ⟨B, A⟩ ↔ A = B)

Theoremmoop2 3979* "At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
B V       ∃*x A = ⟨B, x

Theoremopeqsn 3980 Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.)
A V    &   B V    &   𝐶 V       (⟨A, B⟩ = {𝐶} ↔ (A = B 𝐶 = {A}))

Theoremopeqpr 3981 Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.)
A V    &   B V    &   𝐶 V    &   𝐷 V       (⟨A, B⟩ = {𝐶, 𝐷} ↔ ((𝐶 = {A} 𝐷 = {A, B}) (𝐶 = {A, B} 𝐷 = {A})))

Theoremeuotd 3982* Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.)
(φA V)    &   (φB V)    &   (φ𝐶 V)    &   (φ → (ψ ↔ (𝑎 = A 𝑏 = B 𝑐 = 𝐶)))       (φ∃!x𝑎𝑏𝑐(x = ⟨𝑎, 𝑏, 𝑐 ψ))

Theoremuniop 3983 The union of an ordered pair. Theorem 65 of [Suppes] p. 39. (Contributed by NM, 17-Aug-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
A V    &   B V       A, B⟩ = {A, B}

Theoremuniopel 3984 Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
A V    &   B V       (⟨A, B 𝐶A, B 𝐶)

2.3.4  Ordered-pair class abstractions (cont.)

Theoremopabid 3985 The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(⟨x, y {⟨x, y⟩ ∣ φ} ↔ φ)

Theoremelopab 3986* Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.)
(A {⟨x, y⟩ ∣ φ} ↔ xy(A = ⟨x, y φ))

TheoremopelopabsbALT 3987* The law of concretion in terms of substitutions. Less general than opelopabsb 3988, but having a much shorter proof. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
(⟨z, w {⟨x, y⟩ ∣ φ} ↔ [w / y][z / x]φ)

Theoremopelopabsb 3988* The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
(⟨A, B {⟨x, y⟩ ∣ φ} ↔ [A / x][B / y]φ)

Theorembrabsb 3989* The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.)
𝑅 = {⟨x, y⟩ ∣ φ}       (A𝑅B[A / x][B / y]φ)

Theoremopelopabt 3990* Closed theorem form of opelopab 3999. (Contributed by NM, 19-Feb-2013.)
((xy(x = A → (φψ)) xy(y = B → (ψχ)) (A 𝑉 B 𝑊)) → (⟨A, B {⟨x, y⟩ ∣ φ} ↔ χ))

Theoremopelopabga 3991* The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
((x = A y = B) → (φψ))       ((A 𝑉 B 𝑊) → (⟨A, B {⟨x, y⟩ ∣ φ} ↔ ψ))

Theorembrabga 3992* The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.)
((x = A y = B) → (φψ))    &   𝑅 = {⟨x, y⟩ ∣ φ}       ((A 𝑉 B 𝑊) → (A𝑅Bψ))

Theoremopelopab2a 3993* Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.)
((x = A y = B) → (φψ))       ((A 𝐶 B 𝐷) → (⟨A, B {⟨x, y⟩ ∣ ((x 𝐶 y 𝐷) φ)} ↔ ψ))

Theoremopelopaba 3994* The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
A V    &   B V    &   ((x = A y = B) → (φψ))       (⟨A, B {⟨x, y⟩ ∣ φ} ↔ ψ)

Theorembraba 3995* The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.)
A V    &   B V    &   ((x = A y = B) → (φψ))    &   𝑅 = {⟨x, y⟩ ∣ φ}       (A𝑅Bψ)

Theoremopelopabg 3996* The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
(x = A → (φψ))    &   (y = B → (ψχ))       ((A 𝑉 B 𝑊) → (⟨A, B {⟨x, y⟩ ∣ φ} ↔ χ))

Theorembrabg 3997* The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
(x = A → (φψ))    &   (y = B → (ψχ))    &   𝑅 = {⟨x, y⟩ ∣ φ}       ((A 𝐶 B 𝐷) → (A𝑅Bχ))

Theoremopelopab2 3998* Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)
(x = A → (φψ))    &   (y = B → (ψχ))       ((A 𝐶 B 𝐷) → (⟨A, B {⟨x, y⟩ ∣ ((x 𝐶 y 𝐷) φ)} ↔ χ))

Theoremopelopab 3999* The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.)
A V    &   B V    &   (x = A → (φψ))    &   (y = B → (ψχ))       (⟨A, B {⟨x, y⟩ ∣ φ} ↔ χ)

Theorembrab 4000* The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.)
A V    &   B V    &   (x = A → (φψ))    &   (y = B → (ψχ))    &   𝑅 = {⟨x, y⟩ ∣ φ}       (A𝑅Bχ)

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