 Home Intuitionistic Logic ExplorerTheorem List (p. 29 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 - 2801-2900   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremsbctt 2801 Substitution for a variable not free in a wff does not affect it. (Contributed by Mario Carneiro, 14-Oct-2016.)
((A 𝑉 xφ) → ([A / x]φφ))

Theoremsbcgf 2802 Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 11-Oct-2004.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
xφ       (A 𝑉 → ([A / x]φφ))

Theoremsbc19.21g 2803 Substitution for a variable not free in antecedent affects only the consequent. (Contributed by NM, 11-Oct-2004.)
xφ       (A 𝑉 → ([A / x](φψ) ↔ (φ[A / x]ψ)))

Theoremsbcg 2804* Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 2802. (Contributed by Alan Sare, 10-Nov-2012.)
(A 𝑉 → ([A / x]φφ))

Theoremsbc2iegf 2805* Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Dec-2013.)
xψ    &   yψ    &   x B 𝑊    &   ((x = A y = B) → (φψ))       ((A 𝑉 B 𝑊) → ([A / x][B / y]φψ))

Theoremsbc2ie 2806* Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008.) (Revised by Mario Carneiro, 19-Dec-2013.)
A V    &   B V    &   ((x = A y = B) → (φψ))       ([A / x][B / y]φψ)

Theoremsbc2iedv 2807* Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008.) (Proof shortened by Mario Carneiro, 18-Oct-2016.)
A V    &   B V    &   (φ → ((x = A y = B) → (ψχ)))       (φ → ([A / x][B / y]ψχ))

Theoremsbc3ie 2808* Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Jun-2014.) (Revised by Mario Carneiro, 29-Dec-2014.)
A V    &   B V    &   𝐶 V    &   ((x = A y = B z = 𝐶) → (φψ))       ([A / x][B / y][𝐶 / z]φψ)

Theoremsbccomlem 2809* Lemma for sbccom 2810. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 18-Oct-2016.)
([A / x][B / y]φ[B / y][A / x]φ)

Theoremsbccom 2810* Commutative law for double class substitution. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Mario Carneiro, 18-Oct-2016.)
([A / x][B / y]φ[B / y][A / x]φ)

Theoremsbcralt 2811* Interchange class substitution and restricted quantifier. (Contributed by NM, 1-Mar-2008.) (Revised by David Abernethy, 22-Feb-2010.)
((A 𝑉 yA) → ([A / x]y B φy B [A / x]φ))

Theoremsbcrext 2812* Interchange class substitution and restricted existential quantifier. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
((A 𝑉 yA) → ([A / x]y B φy B [A / x]φ))

Theoremsbcralg 2813* Interchange class substitution and restricted quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
(A 𝑉 → ([A / x]y B φy B [A / x]φ))

Theoremsbcrexg 2814* Interchange class substitution and restricted existential quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
(A 𝑉 → ([A / x]y B φy B [A / x]φ))

Theoremsbcreug 2815* Interchange class substitution and restricted uniqueness quantifier. (Contributed by NM, 24-Feb-2013.)
(A 𝑉 → ([A / x]∃!y B φ∃!y B [A / x]φ))

Theoremsbcabel 2816* Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005.)
xB       (A 𝑉 → ([A / x]{yφ} B ↔ {y[A / x]φ} B))

Theoremrspsbc 2817* Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. This provides an axiom for a predicate calculus for a restricted domain. This theorem generalizes the unrestricted stdpc4 1640 and spsbc 2752. See also rspsbca 2818 and rspcsbela . (Contributed by NM, 17-Nov-2006.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
(A B → (x B φ[A / x]φ))

Theoremrspsbca 2818* Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. (Contributed by NM, 14-Dec-2005.)
((A B x B φ) → [A / x]φ)

Theoremrspesbca 2819* Existence form of rspsbca 2818. (Contributed by NM, 29-Feb-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
((A B [A / x]φ) → x B φ)

Theoremspesbc 2820 Existence form of spsbc 2752. (Contributed by Mario Carneiro, 18-Nov-2016.)
([A / x]φxφ)

Theoremspesbcd 2821 form of spsbc 2752. (Contributed by Mario Carneiro, 9-Feb-2017.)
(φ[A / x]ψ)       (φxψ)

Theoremsbcth2 2822* A substitution into a theorem. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
(x Bφ)       (A B[A / x]φ)

Theoremra5 2823 Restricted quantifier version of Axiom 5 of [Mendelson] p. 69. This is an axiom of a predicate calculus for a restricted domain. Compare the unrestricted stdpc5 1458. (Contributed by NM, 16-Jan-2004.)
xφ       (x A (φψ) → (φx A ψ))

Theoremrmo2ilem 2824* Condition implying restricted "at most one." (Contributed by Jim Kingdon, 14-Jul-2018.)
yφ       (yx A (φx = y) → ∃*x A φ)

Theoremrmo2i 2825* Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017.)
yφ       (y A x A (φx = y) → ∃*x A φ)

Theoremrmo3 2826* Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
yφ       (∃*x A φx A y A ((φ [y / x]φ) → x = y))

Theoremrmob 2827* Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.)
(x = B → (φψ))    &   (x = 𝐶 → (φχ))       ((∃*x A φ (B A ψ)) → (B = 𝐶 ↔ (𝐶 A χ)))

Theoremrmoi 2828* Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
(x = B → (φψ))    &   (x = 𝐶 → (φχ))       ((∃*x A φ (B A ψ) (𝐶 A χ)) → B = 𝐶)

2.1.10  Proper substitution of classes for sets into classes

Syntaxcsb 2829 Extend class notation to include the proper substitution of a class for a set into another class.
class A / xB

Definitiondf-csb 2830* Define the proper substitution of a class for a set into another class. The underlined brackets distinguish it from the substitution into a wff, wsbc 2741, to prevent ambiguity. Theorem sbcel1g 2846 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2855 recreates substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)
A / xB = {y[A / x]y B}

Theoremcsb2 2831* Alternate expression for the proper substitution into a class, without referencing substitution into a wff. Note that x can be free in B but cannot occur in A. (Contributed by NM, 2-Dec-2013.)
A / xB = {yx(x = A y B)}

Theoremcsbeq1 2832 Analog of dfsbcq 2743 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
(A = BA / x𝐶 = B / x𝐶)

Theoremcbvcsb 2833 Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on A. (Contributed by Jeff Hankins, 13-Sep-2009.) (Revised by Mario Carneiro, 11-Dec-2016.)
y𝐶    &   x𝐷    &   (x = y𝐶 = 𝐷)       A / x𝐶 = A / y𝐷

Theoremcbvcsbv 2834* Change the bound variable of a proper substitution into a class using implicit substitution. (Contributed by NM, 30-Sep-2008.) (Revised by Mario Carneiro, 13-Oct-2016.)
(x = yB = 𝐶)       A / xB = A / y𝐶

Theoremcsbeq1d 2835 Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)
(φA = B)       (φA / x𝐶 = B / x𝐶)

Theoremcsbid 2836 Analog of sbid 1639 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
x / xA = A

Theoremcsbeq1a 2837 Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
(x = AB = A / xB)

Theoremcsbco 2838* Composition law for chained substitutions into a class. (Contributed by NM, 10-Nov-2005.)
A / yy / xB = A / xB

Theoremcsbtt 2839 Substitution doesn't affect a constant B (in which x is not free). (Contributed by Mario Carneiro, 14-Oct-2016.)
((A 𝑉 xB) → A / xB = B)

Theoremcsbconstgf 2840 Substitution doesn't affect a constant B (in which x is not free). (Contributed by NM, 10-Nov-2005.)
xB       (A 𝑉A / xB = B)

Theoremcsbconstg 2841* Substitution doesn't affect a constant B (in which x is not free). csbconstgf 2840 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.)
(A 𝑉A / xB = B)

Theoremsbcel12g 2842 Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
(A 𝑉 → ([A / x]B 𝐶A / xB A / x𝐶))

Theoremsbceqg 2843 Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
(A 𝑉 → ([A / x]B = 𝐶A / xB = A / x𝐶))

Theoremsbcnel12g 2844 Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011.)
(A 𝑉 → ([A / x]B𝐶A / xBA / x𝐶))

Theoremsbcne12g 2845 Distribute proper substitution through an inequality. (Contributed by Andrew Salmon, 18-Jun-2011.)
(A 𝑉 → ([A / x]B𝐶A / xBA / x𝐶))

Theoremsbcel1g 2846* Move proper substitution in and out of a membership relation. Note that the scope of [A / x] is the wff B 𝐶, whereas the scope of A / x is the class B. (Contributed by NM, 10-Nov-2005.)
(A 𝑉 → ([A / x]B 𝐶A / xB 𝐶))

Theoremsbceq1g 2847* Move proper substitution to first argument of an equality. (Contributed by NM, 30-Nov-2005.)
(A 𝑉 → ([A / x]B = 𝐶A / xB = 𝐶))

Theoremsbcel2g 2848* Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005.)
(A 𝑉 → ([A / x]B 𝐶B A / x𝐶))

Theoremsbceq2g 2849* Move proper substitution to second argument of an equality. (Contributed by NM, 30-Nov-2005.)
(A 𝑉 → ([A / x]B = 𝐶B = A / x𝐶))

Theoremcsbcomg 2850* Commutative law for double substitution into a class. (Contributed by NM, 14-Nov-2005.)
((A 𝑉 B 𝑊) → A / xB / y𝐶 = B / yA / x𝐶)

Theoremcsbeq2d 2851 Formula-building deduction rule for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
xφ    &   (φB = 𝐶)       (φA / xB = A / x𝐶)

Theoremcsbeq2dv 2852* Formula-building deduction rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
(φB = 𝐶)       (φA / xB = A / x𝐶)

Theoremcsbeq2i 2853 Formula-building inference rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
B = 𝐶       A / xB = A / x𝐶

Theoremcsbvarg 2854 The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005.)
(A 𝑉A / xx = A)

Theoremsbccsbg 2855* Substitution into a wff expressed in terms of substitution into a class. (Contributed by NM, 15-Aug-2007.)
(A 𝑉 → ([A / x]φy A / x{yφ}))

Theoremsbccsb2g 2856 Substitution into a wff expressed in using substitution into a class. (Contributed by NM, 27-Nov-2005.)
(A 𝑉 → ([A / x]φA A / x{xφ}))

Theoremnfcsb1d 2857 Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
(φxA)       (φxA / xB)

Theoremnfcsb1 2858 Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
xA       xA / xB

Theoremnfcsb1v 2859* Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.)
xA / xB

Theoremnfcsbd 2860 Deduction version of nfcsb 2861. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.)
yφ    &   (φxA)    &   (φxB)       (φxA / yB)

Theoremnfcsb 2861 Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
xA    &   xB       xA / yB

Theoremcsbhypf 2862* Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 2580 for class substitution version. (Contributed by NM, 19-Dec-2008.)
xA    &   x𝐶    &   (x = AB = 𝐶)       (y = Ay / xB = 𝐶)

Theoremcsbiebt 2863* Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 2867.) (Contributed by NM, 11-Nov-2005.)
((A 𝑉 x𝐶) → (x(x = AB = 𝐶) ↔ A / xB = 𝐶))

Theoremcsbiedf 2864* Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016.)
xφ    &   (φx𝐶)    &   (φA 𝑉)    &   ((φ x = A) → B = 𝐶)       (φA / xB = 𝐶)

Theoremcsbieb 2865* Bidirectional conversion between an implicit class substitution hypothesis x = AB = 𝐶 and its explicit substitution equivalent. (Contributed by NM, 2-Mar-2008.)
A V    &   x𝐶       (x(x = AB = 𝐶) ↔ A / xB = 𝐶)

Theoremcsbiebg 2866* Bidirectional conversion between an implicit class substitution hypothesis x = AB = 𝐶 and its explicit substitution equivalent. (Contributed by NM, 24-Mar-2013.) (Revised by Mario Carneiro, 11-Dec-2016.)
x𝐶       (A 𝑉 → (x(x = AB = 𝐶) ↔ A / xB = 𝐶))

Theoremcsbiegf 2867* Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 11-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
(A 𝑉x𝐶)    &   (x = AB = 𝐶)       (A 𝑉A / xB = 𝐶)

Theoremcsbief 2868* Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
A V    &   x𝐶    &   (x = AB = 𝐶)       A / xB = 𝐶

Theoremcsbied 2869* Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.)
(φA 𝑉)    &   ((φ x = A) → B = 𝐶)       (φA / xB = 𝐶)

Theoremcsbied2 2870* Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
(φA 𝑉)    &   (φA = B)    &   ((φ x = B) → 𝐶 = 𝐷)       (φA / x𝐶 = 𝐷)

Theoremcsbie2t 2871* Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 2872). (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 13-Oct-2016.)
A V    &   B V       (xy((x = A y = B) → 𝐶 = 𝐷) → A / xB / y𝐶 = 𝐷)

Theoremcsbie2 2872* Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007.)
A V    &   B V    &   ((x = A y = B) → 𝐶 = 𝐷)       A / xB / y𝐶 = 𝐷

Theoremcsbie2g 2873* Conversion of implicit substitution to explicit class substitution. This version of sbcie 2774 avoids a disjointness condition on x and A by substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016.)
(x = yB = 𝐶)    &   (y = A𝐶 = 𝐷)       (A 𝑉A / xB = 𝐷)

Theoremsbcnestgf 2874 Nest the composition of two substitutions. (Contributed by Mario Carneiro, 11-Nov-2016.)
((A 𝑉 yxφ) → ([A / x][B / y]φ[A / xB / y]φ))

Theoremcsbnestgf 2875 Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
((A 𝑉 yx𝐶) → A / xB / y𝐶 = A / xB / y𝐶)

Theoremsbcnestg 2876* Nest the composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
(A 𝑉 → ([A / x][B / y]φ[A / xB / y]φ))

Theoremcsbnestg 2877* Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
(A 𝑉A / xB / y𝐶 = A / xB / y𝐶)

Theoremcsbnest1g 2878 Nest the composition of two substitutions. (Contributed by NM, 23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
(A 𝑉A / xB / x𝐶 = A / xB / x𝐶)

Theoremcsbidmg 2879* Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.)
(A 𝑉A / xA / xB = A / xB)

Theoremsbcco3g 2880* Composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
(x = AB = 𝐶)       (A 𝑉 → ([A / x][B / y]φ[𝐶 / y]φ))

Theoremcsbco3g 2881* Composition of two class substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
(x = AB = 𝐶)       (A 𝑉A / xB / y𝐷 = 𝐶 / y𝐷)

Theoremrspcsbela 2882* Special case related to rspsbc 2817. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.)
((A B x B 𝐶 𝐷) → A / x𝐶 𝐷)

Theoremsbnfc2 2883* Two ways of expressing "x is (effectively) not free in A." (Contributed by Mario Carneiro, 14-Oct-2016.)
(xAyzy / xA = z / xA)

Theoremcsbabg 2884* Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(A 𝑉A / x{yφ} = {y[A / x]φ})

Theoremcbvralcsf 2885 A more general version of cbvralf 2505 that doesn't require A and B to be distinct from x or y. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.)
yA    &   xB    &   yφ    &   xψ    &   (x = yA = B)    &   (x = y → (φψ))       (x A φy B ψ)

Theoremcbvrexcsf 2886 A more general version of cbvrexf 2506 that has no distinct variable restrictions. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.) (Proof shortened by Mario Carneiro, 7-Dec-2014.)
yA    &   xB    &   yφ    &   xψ    &   (x = yA = B)    &   (x = y → (φψ))       (x A φy B ψ)

Theoremcbvreucsf 2887 A more general version of cbvreuv 2513 that has no distinct variable rextrictions. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.)
yA    &   xB    &   yφ    &   xψ    &   (x = yA = B)    &   (x = y → (φψ))       (∃!x A φ∃!y B ψ)

Theoremcbvrabcsf 2888 A more general version of cbvrab 2533 with no distinct variable restrictions. (Contributed by Andrew Salmon, 13-Jul-2011.)
yA    &   xB    &   yφ    &   xψ    &   (x = yA = B)    &   (x = y → (φψ))       {x Aφ} = {y Bψ}

Theoremcbvralv2 2889* Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.)
(x = y → (ψχ))    &   (x = yA = B)       (x A ψy B χ)

Theoremcbvrexv2 2890* Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.)
(x = y → (ψχ))    &   (x = yA = B)       (x A ψy B χ)

2.1.11  Define basic set operations and relations

Syntaxcdif 2891 Extend class notation to include class difference (read: "A minus B").
class (AB)

Syntaxcun 2892 Extend class notation to include union of two classes (read: "A union B").
class (AB)

Syntaxcin 2893 Extend class notation to include the intersection of two classes (read: "A intersect B").
class (AB)

Syntaxwss 2894 Extend wff notation to include the subclass relation. This is read "A is a subclass of B " or "B includes A." When A exists as a set, it is also read "A is a subset of B."
wff AB

Syntaxwpss 2895 Extend wff notation with proper subclass relation.
wff AB

Theoremdifjust 2896* Soundness justification theorem for df-dif 2897. (Contributed by Rodolfo Medina, 27-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
{x ∣ (x A ¬ x B)} = {y ∣ (y A ¬ y B)}

Definitiondf-dif 2897* Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. Contrast this operation with union (AB) (df-un 2899) and intersection (AB) (df-in 2901). Several notations are used in the literature; we chose the convention used in Definition 5.3 of [Eisenberg] p. 67 instead of the more common minus sign to reserve the latter for later use in, e.g., arithmetic. We will use the terminology "A excludes B " to mean AB. We will use "B is removed from A " to mean A ∖ {B} i.e. the removal of an element or equivalently the exclusion of a singleton. (Contributed by NM, 29-Apr-1994.)
(AB) = {x ∣ (x A ¬ x B)}

Theoremunjust 2898* Soundness justification theorem for df-un 2899. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
{x ∣ (x A x B)} = {y ∣ (y A y B)}

Definitiondf-un 2899* Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. Contrast this operation with difference (AB) (df-dif 2897) and intersection (AB) (df-in 2901). (Contributed by NM, 23-Aug-1993.)
(AB) = {x ∣ (x A x B)}

Theoreminjust 2900* Soundness justification theorem for df-in 2901. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
{x ∣ (x A x B)} = {y ∣ (y A y 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-7362
 Copyright terms: Public domain < Previous  Next >