mmtheorems21 - Metamath Proof Explorer

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-10783

Statement List for Metamath Proof Explorer - 2001-2100 - Page 21 of 108

Type	Label	Description
Statement
Proper substitution of classes for sets into classes
Syntax	csb 2001	Extend class notation to include the proper substitution of a class for a set into another class.
class [_A / x]_B
Definition	df-csb 2002	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 1170, to prevent ambiguity. Theorem sbcel1g 2013 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2022 recreates substitution into a wff from this definition.
|- [_A / x]_B = {y | [A / x]y e. B}
Theorem	csbeq1 2003	Analog of dfsbcq 1943 for proper substitution into a class.
|- (A = B -> [_A / x]_C = [_B / x]_C)
Theorem	csbeq1d 2004	Equality deduction for proper substitution into a class.
|- (ph -> A = B)   =>   |- (ph -> [_A / x]_C = [_B / x]_C)
Theorem	csbid 2005	Analog of sbid 1184 for proper substitution into a class.
|- [_x / x]_A = A
Theorem	csbeq1a 2006	Equality theorem for proper substitution into a class.
|- (x = A -> B = [_A / x]_B)
Theorem	csbcog 2007	Composition law for chained substitutions into a class.
|- (A e. C -> [_A / y]_[_y / x]_B = [_A / x]_B)
Theorem	csbexg 2008	The existence of proper substitution into a class.
|- ((A e. C /\ A.x B e. D) -> [_A / x]_B e. V)
Theorem	csbex 2009	The existence of proper substitution into a class.
|- A e. V   &   |- B e. V   =>   |- [_A / x]_B e. V
Theorem	csbconstgf 2010	Substitution doesn't affect a constant B (in which x is not free).
|- (y e. B -> A.x y e. B)   =>   |- (A e. C -> [_A / x]_B = B)
Theorem	sbcel12g 2011	Distribute proper substitution through a membership relation.
|- (A e. D -> ([A / x]B e. C <-> [_A / x]_B e. [_A / x]_C))
Theorem	sbceqdig 2012	Distribute proper substitution through an equality relation.
|- (A e. D -> ([A / x]B = C <-> [_A / x]_B = [_A / x]_C))
Theorem	sbcel1g 2013	Move proper substitution in and out of a membership relation. Note that the scope of [A / x] is the wff B e. C, whereas the scope of [_A / x]_ is the class B.
|- (A e. D -> ([A / x]B e. C <-> [_A / x]_B e. C))
Theorem	sbceq1dig 2014	Move proper substitution to first argument of an equality.
|- (A e. D -> ([A / x]B = C <-> [_A / x]_B = C))
Theorem	sbcel2g 2015	Move proper substitution in and out of a membership relation.
|- (A e. D -> ([A / x]B e. C <-> B e. [_A / x]_C))
Theorem	sbceq2dig 2016	Move proper substitution to second argument of an equality.
|- (A e. D -> ([A / x]B = C <-> B = [_A / x]_C))
Theorem	csbcomg 2017	Commutative law for double substitution into a class.
|- ((A e. R /\ B e. S) -> [_A / x]_[_B / y]_C = [_B / y]_[_A / x]_C)
Theorem	csbeq2d 2018	Formula-building deduction rule for class substitution.
|- (ph -> A.xph)   &   |- (ph -> B = C)   =>   |- ((ph /\ A e. D) -> [_A / x]_B = [_A / x]_C)
Theorem	csbeq2dv 2019	Formula-building deduction rule for class substitution.
|- (ph -> B = C)   =>   |- ((ph /\ A e. D) -> [_A / x]_B = [_A / x]_C)
Theorem	csbeq2i 2020	Formula-building inference rule for class substitution.
|- B = C   =>   |- (A e. D -> [_A / x]_B = [_A / x]_C)
Theorem	csbvarg 2021	The proper substitution of a class for set variable results in the class (if the class exists).
|- (A e. B -> [_A / x]_x = A)
Theorem	sbccsbg 2022	Substitution into a wff expressed in terms of substitution into a class.
|- (A e. B -> ([A / x]ph <-> y e. [_A / x]_{y | ph}))
Theorem	sbccsb2g 2023	Substitution into a wff expressed in using substitution into a class.
|- (A e. B -> ([A / x]ph <-> A e. [_A / x]_{x | ph}))
Theorem	hbcsb1g 2024	Bound-variable hypothesis builder for substitution into a class.
|- (y e. A -> A.x y e. A)   =>   |- (A e. C -> (y e. [_A / x]_B -> A.x y e. [_A / x]_B))
Theorem	hbcsb1 2025	Bound-variable hypothesis builder for substitution into a class.
|- A e. V   &   |- (y e. A -> A.x y e. A)   =>   |- (y e. [_A / x]_B -> A.x y e. [_A / x]_B)
Theorem	hbcsbg 2026	Bound-variable hypothesis builder for substitution into a class.
|- (z e. A -> A.x z e. A)   &   |- (z e. B -> A.x z e. B)   =>   |- (A e. C -> (z e. [_A / y]_B -> A.x z e. [_A / y]_B))
Theorem	hbcsb1gd 2027	Deduction version of hbcsb1g 2024.
|- (ph -> A.xph)   &   |- (ph -> (y e. A -> A.x y e. A))   =>   |- ((ph /\ A e. C) -> (y e. [_A / x]_B -> A.x y e. [_A / x]_B))
Theorem	hbcsbgd 2028	Deduction version of hbcsbg 2026.
|- (ph -> A.xph)   &   |- (ph -> A.yph)   &   |- (ph -> (z e. A -> A.x z e. A))   &   |- (ph -> (z e. B -> A.x z e. B))   =>   |- ((ph /\ A e. C) -> (z e. [_A / y]_B -> A.x z e. [_A / y]_B))
Theorem	csbiegft 2029	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 2031.)
|- ((A e. D /\ A.xA.y(y e. C -> A.x y e. C) /\ A.x(x = A -> B = C)) -> [_A / x]_B = C)
Theorem	csbieb 2030	Bidirectional conversion between an implicit class substitution hypothesis x = A -> B = C and its explicit substitution equivalent.
|- A e. V   &   |- (y e. C -> A.x y e. C)   =>   |- (A.x(x = A -> B = C) <-> [_A / x]_B = C)
Theorem	csbiegf 2031	Conversion of implicit substitution to explicit substitution into a class.
|- (A e. D -> (y e. C -> A.x y e. C))   &   |- (x = A -> B = C)   =>   |- (A e. D -> [_A / x]_B = C)
Theorem	csbief 2032	Conversion of implicit substitution to explicit substitution into a class.
|- A e. V   &   |- (y e. C -> A.x y e. C)   &   |- (x = A -> B = C)   =>   |- [_A / x]_B = C
Theorem	csbie2t 2033	Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 2034).
|- A e. V   &   |- B e. V   =>   |- (A.xA.y((x = A /\ y = B) -> C = D) -> [_A / x]_[_B / y]_C = D)
Theorem	csbie2 2034	Conversion of implicit substitution to explicit substitution into a class.
|- A e. V   &   |- B e. V   &   |- ((x = A /\ y = B) -> C = D)   =>   |- [_A / x]_[_B / y]_C = D
Theorem	csbnestglem 2035	Lemma for csbnestg 2036.
Theorem	csbnestg 2036	Nest the composition of two substitutions.
|- ((A e. R /\ A.x B e. S) -> [_A / x]_[_B / y]_C = [_[_A / x]_B / y]_C)
Theorem	csbnest1g 2037	Nest the composition of two substitutions.
|- ((A e. R /\ A.x B e. S) -> [_A / x]_[_B / x]_C = [_[_A / x]_B / x]_C)
Theorem	sbcnestg 2038	Nest the composition of two substitutions.
|- ((A e. R /\ A.x B e. S) -> ([A / x][B / y]ph <-> [[_A / x]_B / y]ph))
Theorem	csbidmg 2039	Idempotent law for class substitutions.
|- (A e. C -> [_A / x]_[_A / x]_B = [_A / x]_B)
Theorem	csbco3g 2040	Composition of two class substitutions.
|- (x = A -> B = D)   =>   |- ((A e. R /\ A.x B e. S) -> [_A / x]_[_B / y]_C = [_D / y]_C)
Theorem	sbcco3g 2041	Composition of two substitutions.
|- (x = A -> B = C)   =>   |- ((A e. R /\ A.x B e. S) -> ([A / x][B / y]ph <-> [C / y]ph))
Theorem	ra4csbela 2042	Special case related to ra4sbc 1997. (The proof was shortened by Eric Schmidt, 17-Jan-2007.)
|- ((A e. B /\ A.x e. B C e. D) -> [_A / x]_C e. D)
Theorem	csbabg 2043	Move substitution into a class abstraction.
|- (A e. B -> [_A / x]_{y | ph} = {y | [A / x]ph})
Define basic set operations and relations
Syntax	cdif 2044	Extend class notation to include class difference (read: "A minus B").
class (A \ B)
Syntax	cun 2045	Extend class notation to include union of two classes (read: "A union B").
class (A u. B)
Syntax	cin 2046	Extend class notation to include the intersection of two classes (read: "A intersect B").
class (A i^i B)
Syntax	wss 2047	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 A (_ B
Syntax	wpss 2048	Extend wff notation with proper subclass relation.
wff A (. B
Definition	df-dif 2049	Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. 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 A \ B. 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.
|- (A \ B) = {x | (x e. A /\ -. x e. B)}
Definition	df-un 2050	Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For an alternate definition in terms of class difference, requiring no dummy variables, see dfun2 2243. For union defined in terms of intersection, see dfun3 2246.
|- (A u. B) = {x | (x e. A \/ x e. B)}
Definition	df-in 2051	Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 2244 and dfin4 2248. For intersection defined in terms of union, see dfin3 2247.
|- (A i^i B) = {x | (x e. A /\ x e. B)}
Theorem	dfin5 2052	Alternate definition for the intersection of two classes.
|- (A i^i B) = {x e. A | x e. B}
Definition	df-ss 2053	Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For a more traditional defini