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

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

Type	Label	Description
Statement
Theorem	csbid 2001	Analog of sbid 1182 for proper substitution into a class.
|- [_x / x]_A = A
Theorem	csbeq1a 2002	Equality theorem for proper substitution into a class.
|- (x = A -> B = [_A / x]_B)
Theorem	csbcog 2003	Composition law for chained substitutions into a class.
|- (A e. C -> [_A / y]_[_y / x]_B = [_A / x]_B)
Theorem	csbexg 2004	The existence of proper substitution into a class.
|- ((A e. C /\ A.x B e. D) -> [_A / x]_B e. V)
Theorem	csbex 2005	The existence of proper substitution into a class.
|- A e. V   &   |- B e. V   =>   |- [_A / x]_B e. V
Theorem	csbconstgf 2006	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 2007	Distribute proper substitution through a membership relation.
|- (A e. D -> ([A / x]B e. C <-> [_A / x]_B e. [_A / x]_C))
Theorem	sbceqdig 2008	Distribute proper substitution through an equality relation.
|- (A e. D -> ([A / x]B = C <-> [_A / x]_B = [_A / x]_C))
Theorem	sbcel1g 2009	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 2010	Move proper substitution to first argument of an equality.
|- (A e. D -> ([A / x]B = C <-> [_A / x]_B = C))
Theorem	sbcel2g 2011	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 2012	Move proper substitution to second argument of an equality.
|- (A e. D -> ([A / x]B = C <-> B = [_A / x]_C))
Theorem	csbcomg 2013	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 2014	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 2015	Formula-building deduction rule for class substitution.
|- (ph -> B = C)   =>   |- ((ph /\ A e. D) -> [_A / x]_B = [_A / x]_C)
Theorem	csbeq2i 2016	Formula-building inference rule for class substitution.
|- B = C   =>   |- (A e. D -> [_A / x]_B = [_A / x]_C)
Theorem	csbvarg 2017	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 2018	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 2019	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 2020	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 2021	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 2022	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 2023	Deduction version of hbcsb1g 2020.
|- (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 2024	Deduction version of hbcsbg 2022.
|- (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 2025	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 2027.)
|- ((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 2026	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 2027	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 2028	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 2029	Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 2030).
|- A e. V   &   |- B e. V   =>   |- (A.xA.y((x = A /\ y = B) -> C = D) -> [_A / x]_[_B / y]_C = D)
Theorem	csbie2 2030	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 2031	Lemma for csbnestg 2032.
Theorem	csbnestg 2032	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 2033	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 2034	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 2035	Idempotent law for class substitutions.
|- (A e. C -> [_A / x]_[_A / x]_B = [_A / x]_B)
Theorem	csbco3g 2036	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 2037	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 2038	Special case related to ra4sbc 1993. (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 2039	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 2040	Extend class notation to include class difference (read: "A minus B").
class (A \ B)
Syntax	cun 2041	Extend class notation to include union of two classes (read: "A union B").
class (A u. B)
Syntax	cin 2042	Extend class notation to include the intersection of two classes (read: "A intersect B").
class (A i^i B)
Syntax	wss 2043	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 2044	Extend wff notation with proper subclass relation.
wff A (. B
Definition	df-dif 2045	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 2046	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 2239. For union defined in terms of intersection, see dfun3 2242.
|- (A u. B) = {x | (x e. A \/ x e. B)}
Definition	df-in 2047	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 2240 and dfin4 2244. For intersection defined in terms of union, see dfin3 2243.
|- (A i^i B) = {x | (x e. A /\ x e. B)}
Theorem	dfin5 2048	Alternate definition for the intersection of two classes.
|- (A i^i B) = {x e. A | x e. B}
Definition	df-ss 2049	Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For a more traditional definition, but requiring a dummy variable, see dfss2 2054. Other possible definitions are given by dfss3 2055, dfss4 2238, sspss 2141, ssequn1 2196, ssequn2 2199, sseqin2 2225, and ssdif0 2323.
|- (A (_ B <-> (A i^i B) = A)
Theorem	dfss 2050	A frequently-used variant of subclass definition df-ss 2049.
|- (A (_ B <-> A = (A i^i B))
Definition	df-pss 2051	Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. Other possible definitions are given by dfpss2 2129 and dfpss3 2130.
|- (A (. B <-> (A (_ B /\ A =/= B))
Theorem	dfdif2 2052	Alternate definition of class difference.
|- (A \ B) = {x e. A | -. x e. B}
Theorem	eldif 2053	Expansion of membership in a class difference.
|- (A e. (B \ C) <-> (A