HomeHome Intuitionistic Logic Explorer
Theorem List (p. 40 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 - 3901-4000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremel 3901* 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 3902 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 3903 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 3904* 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 3905 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 3906 and new proofs should use snexg 3906 instead. (Contributed by Jim Kingdon, 26-Jan-2019.) (New usage is discouraged.) TODO: remove in favor of snexg 3906.
(A V → {A} V)
 
Theoremsnexg 3906 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 3907 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 3908 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 3909 The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.)
{∅} V
 
Theorempp0ex 3910 {∅, {∅}} (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.)
{∅, {∅}} V
 
Theoremord3ex 3911 The ordinal number 3 is a set, proved without the Axiom of Union. (Contributed by NM, 2-May-2009.)
{∅, {∅}, {∅, {∅}}} V
 
Theoremdtruarb 3912* 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 4217 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 3913 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 3914* 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 3848). (Contributed by NM, 14-Nov-2006.)
zw((w = x w = y) → w z)
 
Theoremzfpair2 3915 Derive the abbreviated version of the Axiom of Pairing from ax-pr 3914. (Contributed by NM, 14-Nov-2006.)
{x, y} V
 
TheoremprexgOLD 3916 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 3450, prprc1 3448, and prprc2 3449. This is a special case of prexg 3917 and new proofs should use prexg 3917 instead. (Contributed by Jim Kingdon, 25-Jul-2019.) (New usage is discouraged.) TODO: remove in favor of prexg 3917.
((A V B V) → {A, B} V)
 
Theoremprexg 3917 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 3450, prprc1 3448, and prprc2 3449. (Contributed by Jim Kingdon, 16-Sep-2018.)
((A 𝑉 B 𝑊) → {A, B} V)
 
Theoremsnelpwi 3918 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 3919 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 3920 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 3921* 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 3922 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 3923 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 3924 Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.)
(A B → 𝒫 A 𝒫 𝒫 B)
 
Theorempwtr 3925 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 3926* An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.)
(ABx(xAxB))
 
Theoremssext 3927* 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 3928* Negation of subclass relationship. Compare nssr 2976. (Contributed by Jim Kingdon, 17-Sep-2018.)
(x(xA ¬ xB) → ¬ AB)
 
Theorempweqb 3929 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 3930* 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 3931 The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.)
(∃!xφ → {xφ} V)
 
Theoremmss 3932* 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 3933* 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 3934 An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.)
((A 𝑉 B 𝑊) → ⟨A, B V)
 
TheoremopexgOLD 3935 An ordered pair of sets is a set. This is a special case of opexg 3934 and new proofs should use opexg 3934 instead. (Contributed by Jim Kingdon, 19-Sep-2018.) (New usage is discouraged.) TODO: remove in favor of opexg 3934.
((A V B V) → ⟨A, B V)
 
Theoremopex 3936 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 3937 An ordered triple of sets is a set. (Contributed by Jim Kingdon, 19-Sep-2018.)
((A 𝑈 B 𝑉 𝐶 𝑊) → ⟨A, B, 𝐶 V)
 
Theoremelop 3938 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 3939 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 3940 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 3941* 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 3942 An ordered pair is nonempty if the arguments are sets (it is also inhabited; see opm 3941). (Contributed by Mario Carneiro, 26-Apr-2015.)
A V    &   B V       A, B⟩ ≠ ∅
 
Theoremopth1 3943 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 3944 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 3945 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 3946 Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.)
((𝐶 𝑉 𝐷 𝑊) → (⟨A, B⟩ = ⟨𝐶, 𝐷⟩ ↔ (A = 𝐶 B = 𝐷)))
 
Theoremopth2 3947 Ordered pair theorem. (Contributed by NM, 21-Sep-2014.)
𝐶 V    &   𝐷 V       (⟨A, B⟩ = ⟨𝐶, 𝐷⟩ ↔ (A = 𝐶 B = 𝐷))
 
Theoremotth2 3948 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 3949 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 3950* 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 3951* 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 3952* Closed theorem form of copsex2g 3953. (Contributed by NM, 17-Feb-2013.)
((xy((x = A y = B) → (φψ)) (A 𝑉 B 𝑊)) → (xy(⟨A, B⟩ = ⟨x, y φ) ↔ ψ))
 
Theoremcopsex2g 3953* Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.)
((x = A y = B) → (φψ))       ((A 𝑉 B 𝑊) → (xy(⟨A, B⟩ = ⟨x, y φ) ↔ ψ))
 
Theoremcopsex4g 3954* 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 3955 A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
¬ ∅ A, B
 
Theoremopeqex 3956 Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.)
(⟨A, B⟩ = ⟨𝐶, 𝐷⟩ → ((A V B V) ↔ (𝐶 V 𝐷 V)))
 
Theoremopcom 3957 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 3958* "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 3959 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 3960 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 3961* Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.)
(φA V)    &   (φB V)    &   (φ𝐶 V)    &   (φ → (ψ ↔ (𝑎 = A 𝑏 = B 𝑐 = 𝐶)))       (φ∃!x𝑎𝑏𝑐(x = ⟨𝑎, 𝑏, 𝑐 ψ))
 
Theoremuniop 3962 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 3963 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 3964 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 3965* Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.)
(A {⟨x, y⟩ ∣ φ} ↔ xy(A = ⟨x, y φ))
 
TheoremopelopabsbALT 3966* The law of concretion in terms of substitutions. Less general than opelopabsb 3967, 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 3967* 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 3968* The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.)
𝑅 = {⟨x, y⟩ ∣ φ}       (A𝑅B[A / x][B / y]φ)
 
Theoremopelopabt 3969* Closed theorem form of opelopab 3978. (Contributed by NM, 19-Feb-2013.)
((xy(x = A → (φψ)) xy(y = B → (ψχ)) (A 𝑉 B 𝑊)) → (⟨A, B {⟨x, y⟩ ∣ φ} ↔ χ))
 
Theoremopelopabga 3970* 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 3971* 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 3972* 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 3973* 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 3974* 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 3975* 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 3976* 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 3977* 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 3978* 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 3979* 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χ)
 
Theoremopelopabaf 3980* The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 3978 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
xψ    &   yψ    &   A V    &   B V    &   ((x = A y = B) → (φψ))       (⟨A, B {⟨x, y⟩ ∣ φ} ↔ ψ)
 
Theoremopelopabf 3981* The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 3978 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.)
xψ    &   yχ    &   A V    &   B V    &   (x = A → (φψ))    &   (y = B → (ψχ))       (⟨A, B {⟨x, y⟩ ∣ φ} ↔ χ)
 
Theoremssopab2 3982 Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.)
(xy(φψ) → {⟨x, y⟩ ∣ φ} ⊆ {⟨x, y⟩ ∣ ψ})
 
Theoremssopab2b 3983 Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
({⟨x, y⟩ ∣ φ} ⊆ {⟨x, y⟩ ∣ ψ} ↔ xy(φψ))
 
Theoremssopab2i 3984 Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)
(φψ)       {⟨x, y⟩ ∣ φ} ⊆ {⟨x, y⟩ ∣ ψ}
 
Theoremssopab2dv 3985* Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
(φ → (ψχ))       (φ → {⟨x, y⟩ ∣ ψ} ⊆ {⟨x, y⟩ ∣ χ})
 
Theoremeqopab2b 3986 Equivalence of ordered pair abstraction equality and biconditional. (Contributed by Mario Carneiro, 4-Jan-2017.)
({⟨x, y⟩ ∣ φ} = {⟨x, y⟩ ∣ ψ} ↔ xy(φψ))
 
Theoremopabm 3987* Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon, 29-Sep-2018.)
(z z {⟨x, y⟩ ∣ φ} ↔ xyφ)
 
Theoremiunopab 3988* Move indexed union inside an ordered-pair abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.)
z A {⟨x, y⟩ ∣ φ} = {⟨x, y⟩ ∣ z A φ}
 
2.3.5  Power class of union and intersection
 
Theorempwin 3989 The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
𝒫 (AB) = (𝒫 A ∩ 𝒫 B)
 
Theorempwunss 3990 The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
(𝒫 A ∪ 𝒫 B) ⊆ 𝒫 (AB)
 
Theorempwssunim 3991 The power class of the union of two classes is a subset of the union of their power classes, if one class is a subclass of the other. One direction of Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by Jim Kingdon, 30-Sep-2018.)
((AB BA) → 𝒫 (AB) ⊆ (𝒫 A ∪ 𝒫 B))
 
Theorempwundifss 3992 Break up the power class of a union into a union of smaller classes. (Contributed by Jim Kingdon, 30-Sep-2018.)
((𝒫 (AB) ∖ 𝒫 A) ∪ 𝒫 A) ⊆ 𝒫 (AB)
 
Theorempwunim 3993 The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of [Enderton] p. 28. (Contributed by Jim Kingdon, 30-Sep-2018.)
((AB BA) → 𝒫 (AB) = (𝒫 A ∪ 𝒫 B))
 
2.3.6  Epsilon and identity relations
 
Syntaxcep 3994 Extend class notation to include the epsilon relation.
class E
 
Syntaxcid 3995 Extend the definition of a class to include identity relation.
class I
 
Definitiondf-eprel 3996* Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30. The epsilon relation and set membership are the same, that is, (A E BA B) when B is a set by epelg 3997. Thus, 5 E { 1 , 5 }. (Contributed by NM, 13-Aug-1995.)
E = {⟨x, y⟩ ∣ x y}
 
Theoremepelg 3997 The epsilon relation and membership are the same. General version of epel 3999. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.)
(B 𝑉 → (A E BA B))
 
Theoremepelc 3998 The epsilon relationship and the membership relation are the same. (Contributed by Scott Fenton, 11-Apr-2012.)
B V       (A E BA B)
 
Theoremepel 3999 The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
(x E yx y)
 
Definitiondf-id 4000* Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 I 5 and ¬ 4 I 5. (Contributed by NM, 13-Aug-1995.)
I = {⟨x, y⟩ ∣ x = y}
    < Previous  Next >

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 >