mmtheorems34 - 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-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 3301-3400 - Page 34 of 175

Type	Label	Description
Statement
Theorem	iunxdif2 3301	Indexed union with a class difference as its index.
|- (x = y -> C = D)   =>   |- (A.x e. A E.y e. (A \ B)C C_ D -> U_y e. (A \ B)D = U_x e. A C)
Theorem	ssiin 3302	Subset theorem for an indexed intersection. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- (C C_ |^|_x e. A B <-> A.x e. A C C_ B)
Theorem	ssiinOLD 3303	Subset theorem for an indexed intersection.
|- (C C_ |^|_x e. A B <-> A.x e. A C C_ B)
Theorem	iinss 3304	Subset implication for an indexed intersection. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- (E.x e. A B C_ C -> |^|_x e. A B C_ C)
Theorem	iinssOLD 3305	Subset implication for an indexed intersection.
|- (E.x e. A B C_ C -> |^|_x e. A B C_ C)
Theorem	uniiun 3306	Class union in terms of indexed union. Definition of [Stoll] p. 43.
|- U.A = U_x e. A x
Theorem	intiin 3307	Class intersection in terms of indexed intersection. Definition of [Stoll] p. 44.
|- |^|A = |^|_x e. A x
Theorem	iunid 3308	An indexed union of singletons recovers the index set.
|- U_x e. A {x} = A
Theorem	iun0 3309	An indexed union of the empty set is empty. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- U_x e. A (/) = (/)
Theorem	iun0OLD 3310	An indexed union of the empty set is empty.
|- U_x e. A (/) = (/)
Theorem	0iun 3311	An empty indexed union is empty. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- U_x e. (/) A = (/)
Theorem	0iunOLD 3312	An empty indexed union is empty.
|- U_x e. (/) A = (/)
Theorem	0iin 3313	An empty indexed intersection is the universal class.
|- |^|_x e. (/) A = _V
Theorem	viin 3314	Indexed intersection with a universal index class. When A doesn't depend on x, this evaluates to A by 19.3 1378 and abid2 2011. When A = x, this evaluates to (/) by intiin 3307 and intv 3479.
|- |^|_x e. _V A = {y | A.x y e. A}
Theorem	iunn0 3315	There is a non-empty class in an indexed collection B(x) iff the indexed union of them is non-empty. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- (E.x e. A B =/= (/) <-> U_x e. A B =/= (/))
Theorem	iunn0OLD 3316	There is a non-empty class in an indexed collection B(x) iff the indexed union of them is non-empty.
|- (E.x e. A B =/= (/) <-> U_x e. A B =/= (/))
Theorem	iinab 3317	Indexed intersection of a class builder.
|- |^|_x e. A {y | ph} = {y | A.x e. A ph}
Theorem	iinrab 3318	Indexed intersection of a restricted class builder.
|- (A =/= (/) -> |^|_x e. A {y e. B | ph} = {y e. B | A.x e. A ph})
Theorem	iinrab2 3319	Indexed intersection of a restricted class builder.
|- (|^|_x e. A {y e. B | ph} i^i B) = {y e. B | A.x e. A ph}
Theorem	iunin2 3320	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 3306 to recover Enderton's theorem.
|- U_x e. A (B i^i C) = (B i^i U_x e. A C)
Theorem	iinun2 3321	Indexed intersection of union. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 3307 to recover Enderton's theorem.
|- |^|_x e. A (B u. C) = (B u. |^|_x e. A C)
Theorem	iundif2 3322	Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use intiin 3307 to recover Enderton's theorem.
|- U_x e. A (B \ C) = (B \ |^|_x e. A C)
Theorem	2iunin 3323	Rearrange indexed unions over intersection.
|- U_x e. A U_y e. B (C i^i D) = (U_x e. A C i^i U_y e. B D)
Theorem	iindif2 3324	Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use uniiun 3306 to recover Enderton's theorem.
|- (A =/= (/) -> |^|_x e. A (B \ C) = (B \ U_x e. A C))
Theorem	iinxsng 3325	A singleton index picks out an instance of an indexed intersection's argument.
|- (x = A -> B = C)   =>   |- (A e. D -> |^|_x e. {A}B = C)
Theorem	iinxprg 3326	Indexed intersection with an unordered pair index.
|- (x = A -> C = D)   &   |- (x = B -> C = E)   =>   |- ((A e. F /\ B e. G) -> |^|_x e. {A, B}C = (D i^i E))
Theorem	iunxsn 3327	A singleton index picks out an instance of an indexed union's argument.
|- A e. _V   &   |- (x = A -> B = C)   =>   |- U_x e. {A}B = C
Theorem	iunun 3328	Separate a union in an indexed union.
|- U_x e. A (B u. C) = (U_x e. A B u. U_x e. A C)
Theorem	iunxun 3329	Separate a union in the index of an indexed union.
|- U_x e. (A u. B)C = (U_x e. A C u. U_x e. B C)
Theorem	iinuni 3330	A relationship involving union and indexed intersection. Exercise 23 of [Enderton] p. 33.
|- (A u. |^|B) = |^|_x e. B (A u. x)
Theorem	iununi 3331	A relationship involving union and indexed union. Exercise 25 of [Enderton] p. 33. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- ((B = (/) -> A = (/)) <-> (A u. U.B) = U_x e. B (A u. x))
Theorem	iununiOLD 3332	A relationship involving union and indexed union. Exercise 25 of [Enderton] p. 33.
|- ((B = (/) -> A = (/)) <-> (A u. U.B) = U_x e. B (A u. x))
Theorem	sspwuni 3333	Subclass relationship for power class and union.
|- (A C_ ~PB <-> U.A C_ B)
Theorem	pwssb 3334	Two ways to express a collection of subclasses.
|- (A C_ ~PB <-> A.x e. A x C_ B)
Theorem	elpwuni 3335	Relationship for power class and union.
|- (B e. A -> (A C_ ~PB <-> U.A = B))
Theorem	iinpw 3336	The power class of an intersection in terms of indexed intersection. Exercise 24(a) of [Enderton] p. 33.
|- ~P|^|A = |^|_x e. A ~Px
Theorem	iunpwss 3337	Inclusion of an indexed union of a power class in the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33.
|- U_x e. A ~Px C_ ~PU.A
Binary relations
Syntax	wbr 3338	Extend wff notation to include the general binary relation predicate. Note that the syntax is simply three class symbols in a row. Since binary relations are the only possible wff expressions consisting of three class expressions in a row, the syntax is unambiguous. (For an example of how syntax could become ambiguous if we are not careful, see the comment in cneg 6446.)
wff ARB
Definition	df-br 3339	Define a general binary relation. Note that the syntax is simply three class symbols in a row. Definition 6.18 of [TakeutiZaring] p. 29 generalized to arbitrary classes. Class R normally denotes a relation such as "< " that compares two classes A and B, which might be numbers such as 1 and 2. This definition is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when R is a proper class.
|- (ARB <-> <.A, B>. e. R)
Theorem	breq 3340	Equality theorem for binary relations.
|- (R = S -> (ARB <-> ASB))
Theorem	breq1 3341	Equality theorem for a binary relation.
|- (A = B -> (ARC <-> BRC))
Theorem	breq2 3342	Equality theorem for a binary relation.
|- (A = B -> (CRA <-> CRB))
Theorem	breq12 3343	Equality theorem for a binary relation.
|- ((A = B /\ C = D) -> (ARC <-> BRD))
Theorem	breqi 3344	Equality inference for binary relations.
|- R = S   =>   |- (ARB <-> ASB)
Theorem	breq1i 3345	Equality inference for a binary relation.
|- A = B   =>   |- (ARC <-> BRC)
Theorem	breq2i 3346	Equality inference for a binary relation.
|- A = B   =>   |- (CRA <-> CRB)
Theorem	breq12i 3347	Equality inference for a binary relation. (The proof was shortened by Eric Schmidt, 4-Apr-2007.)
|- A = B   &   |- C = D   =>   |- (ARC <-> BRD)
Theorem	breq1d 3348	Equality deduction for a binary relation.
|- (ph -> A = B)   =>   |- (ph -> (ARC <-> BRC))
Theorem	breqd 3349	Equality deduction for a binary relation.
|- (ph -> A = B)   =>   |- (ph -> (CAD <-> CBD))
Theorem	breq2d 3350	Equality deduction for a binary relation.
|- (ph -> A = B)   =>   |- (ph -> (CRA <-> CRB))
Theorem	breq12d 3351	Equality deduction for a binary relation. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (ARC <-> BRD))
Theorem	breq12dOLD 3352	Equality deduction for a binary relation.
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (ARC <-> BRD))
Theorem	breq123d 3353	Equality deduction for a binary relation.
|- (ph -> A = B)   &   |- (ph -> R = S)   &   |- (ph -> C = D)   =>   |- (ph -> (ARC <-> BSD))
Theorem	breqan12d 3354	Equality deduction for a binary relation.
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ph /\ ps) -> (ARC <-> BRD))
Theorem	breqan12rd 3355	Equality deduction for a binary relation.
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ps /\ ph) -> (ARC <-> BRD))
Theorem	eqbrtri 3356	Substitution of equal classes into a binary relation.
|- A = B   &   |- BRC   =>   |- ARC
Theorem	eqbrtrd 3357	Substitution of equal classes into a binary relation.
|- (ph -> A = B)   &   |- (ph -> BRC)   =>   |- (ph -> ARC)
Theorem	eqbrtrri 3358	Substitution of equal classes into a binary relation.
|- A = B   &   |- ARC   =>   |- BRC
Theorem	eqbrtrrd 3359	Substitution of equal classes into a binary relation.
|- (ph -> A = B)   &   |- (ph -> ARC)   =>   |- (ph -> BRC)
Theorem	breqtri 3360	Substitution of equal classes into a binary relation.
|- ARB   &   |- B = C   =>   |- ARC
Theorem	breqtrd 3361	Substitution of equal classes into a binary relation.
|- (ph -> ARB)   &   |- (ph -> B = C)   =>   |- (ph -> ARC)
Theorem	breqtrri 3362	Substitution of equal classes into a binary relation.
|- ARB   &   |- C = B   =>   |- ARC
Theorem	breqtrrd 3363	Substitution of equal classes into a binary relation.
|- (ph -> ARB)   &   |- (ph -> C = B)   =>   |- (ph -> ARC)
Theorem	3brtr3i 3364	Substitution of equality into both sides of a binary relation.
|- ARB   &   |- A = C   &   |- B = D   =>   |- CRD
Theorem	3brtr4i 3365	Substitution of equality into both sides of a binary relation.
|- ARB   &   |- C = A   &   |- D = B   =>   |- CRD
Theorem	3brtr3d 3366	Substitution of equality into both sides of a binary relation.
|- (ph -> ARB)   &   |- (ph -> A = C)   &   |- (ph -> B = D)   =>   |- (ph -> CRD)
Theorem	3brtr4d 3367	Substitution of equality into both sides of a binary relation.
|- (ph -> ARB)   &   |- (ph -> C = A)   &   |- (ph -> D = B)   =>   |- (ph -> CRD)
Theorem	3brtr3g 3368	Substitution of equality into both sides of a binary relation.
|- (ph -> ARB)   &   |- A = C   &   |- B = D   =>   |- (ph -> CRD)
Theorem	3brtr4g 3369	Substitution of equality into both sides of a binary relation.
|- (ph -> ARB)   &   |- C = A   &   |- D = B   =>   |- (ph -> CRD)
Theorem	syl5eqbr 3370	A chained equality inference for a binary relation.
|- (ph -> ARB)   &   |- C = A   =>   |- (ph -> CRB)
Theorem	syl5eqbrr 3371	A chained equality inference for a binary relation.
|- (ph -> ARB)   &   |- A = C   =>   |- (ph -> CRB)
Theorem	syl5breq 3372	A chained equality inference for a binary relation.
|- (ph -> A = B)   &   |- CRA   =>   |- (ph -> CRB)
Theorem	syl5breqr 3373	A chained equality inference for a binary relation.
|- (ph -> B = A)   &   |- CRA   =>   |- (ph -> CRB)
Theorem	syl6eqbr 3374	A chained equality inference for a binary relation.
|- (ph -> A = B)   &   |- BRC   =>   |- (ph -> ARC)
Theorem	syl6eqbrr 3375	A chained equality inference for a binary relation.
|- (ph -> B = A)   &   |- BRC   =>   |- (ph -> ARC)
Theorem	syl6breq 3376	A chained equality inference for a binary relation.
|- (ph -> ARB)   &   |- B = C   =>   |- (ph -> ARC)
Theorem	syl6breqr 3377	A chained equality inference for a binary relation.
|- (ph -> ARB)   &   |- C = B   =>   |- (ph -> ARC)
Theorem	ssbrd 3378	Deduction from a subclass relationship of binary relations.
|- (ph -> A C_ B)   =>   |- (ph -> (CAD -> CBD))
Theorem	ssbri 3379	Inference from a subclass relationship of binary relations. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
|- A C_ B   =>   |- (CAD -> CBD)
Theorem	ssbriOLD 3380	Inference from a subclass relationship of binary relations.
|- A C_ B   =>   |- (CAD -> CBD)
Theorem	hbbr 3381	Bound-variable hypothesis builder for binary relation.
|- (y e. A -> A.x y e. A)   &   |- (y e. R -> A.x y e. R)   &   |- (y e. B -> A.x y e. B)   =>   |- (ARB -> A.x ARB)
Theorem	hbbrd 3382	Deduction version of bound-variable hypothesis builder hbbr 3381. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
|- (ph -> A.xph)   &   |- (ph -> (y e. A -> A.x y e. A))   &   |- (ph -> (y e. R -> A.x y e. R))   &   |- (ph -> (y e. B -> A.x y e. B))   =>   |- (ph -> (ARB -> A.x ARB))
Theorem	hbbrdOLD 3383	Deduction version of bound-variable hypothesis builder hbbr 3381.
|- (ph -> A.xph)   &   |- (ph -> (y e. A -> A.x y e. A))   &   |- (ph -> (y e. R -> A.x y e. R))   &   |- (ph -> (y e. B -> A.x y e. B))   =>   |- (ph -> (ARB -> A.x ARB))
Theorem	brab1 3384	Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.)
|- (xRA <-> x e. {z | zRA})
Theorem	brab1OLD 3385	Relationship between a binary relation and a class abstraction.
|- (xRy <-> x e. {z | zRy})
Theorem	brprc 3386	A property of proper class as the second argument of a binary relation.
|- (-. B e. _V -> (ARB <-> ARA))
Theorem	brun 3387	The union of two binary relations.
|- (A(R u. S)B <-> (ARB \/ ASB))
Theorem	brin 3388	The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
|- (A(R i^i S)B <-> (ARB /\ ASB))
Theorem	brdif 3389	The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
|- (A(R \ S)B <-> (ARB /\ -. ASB))
Theorem	sbcbrg 3390	Move substitution in and out of a binary relation. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
|- (A e. D -> ([A / x]BRC <-> [_A / x]_B[_A / x]_R[_A / x]_C))
Theorem	sbcbrgOLD 3391	Move substitution in and out of a binary relation.
|- (A e. D -> ([A / x]BRC <-> [_A / x]_B[_A / x]_R[_A / x]_C))
Theorem	sbcbr12g 3392	Move substitution in and out of a binary relation.
|- (A e. D -> ([A / x]BRC <-> [_A / x]_BR[_A / x]_C))
Theorem	sbcbr1g 3393	Move substitution in and out of a binary relation.
|- (A e. D -> ([A / x]BRC <-> [_A / x]_BRC))
Theorem	sbcbr2g 3394	Move substitution in and out of a binary relation.
|- (A e. D -> ([A / x]BRC <-> BR[_A / x]_C))
Ordered-pair class abstractions (class builders)
Syntax	copab 3395	Extend class notation to include ordered-pair class abstraction (class builder).
class {<.x, y>. | ph}
Definition	df-opab 3396	Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually x and y are distinct, although the definition doesn't strictly require it (see dfid2 3588 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 5053.
|- {<.x, y>. | ph} = {z | E.xE.y(z = <.x, y>. /\ ph)}
Theorem	opabss 3397	The collection of ordered pairs in a class is a subclass of it. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
|- {<.x, y>. | xRy} C_ R
Theorem	opabssOLD 3398	The collection of ordered pairs in a class is a subclass of it.
|- {<.x, y>. | xRy} C_ R
Theorem	opabbid 3399	Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
|- (ph -> A.xph)   &   |- (ph -> A.yph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> {<.x, y>. | ps} = {<.x, y>. | ch})
Theorem	opabbidOLD 3400	Equivalent wff's yield equal ordered-pair class abstractions (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> A.yph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> {<.x, y>. | ps} = {<.x, y>. | ch})