Metamath Proof Explorer - mmtheorems12

Jump to page: 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-5787

Statement List for Metamath Proof Explorer - 1101-1200 - Page 12 of 58

Type	Label	Description
Statement
Theorem	cleqri 1101	Infer equality of sets from equivalence of membership.
|- (x e. A <-> x e. B)   =>   |- A = B
Theorem	cleqid 1102	Class identity law (reflexivity of class equality). Theorem 6.4 of [Quine] p. 41.
|- A = A
Theorem	cleqcom 1103	Commutative law for class equality. Theorem 6.5 of [Quine] p. 41.
|- (A = B <-> B = A)
Theorem	cleqcoms 1104	Inference applying commutative law for class equality to an antecedent.
|- (A = B -> ph)   =>   |- (B = A -> ph)
Theorem	cleqcomi 1105	Inference from commutative law for class equality.
|- A = B   =>   |- B = A
Theorem	cleqcomd 1106	Deduction from commutative law for class equality.
|- (ph -> A = B)   =>   |- (ph -> B = A)
Theorem	cleq1 1107	Equality implies equivalence of equalities.
|- (A = B -> (A = C <-> B = C))
Theorem	cleq1i 1108	Inference from equality to equivalence of equalities.
|- A = B   =>   |- (A = C <-> B = C)
Theorem	cleq1d 1109	Deduction from equality to equivalence of equalities.
|- (ph -> A = B)   =>   |- (ph -> (A = C <-> B = C))
Theorem	cleq2 1110	Equality implies equivalence of equalities.
|- (A = B -> (C = A <-> C = B))
Theorem	cleq2i 1111	Inference from equality to equivalence of equalities.
|- A = B   =>   |- (C = A <-> C = B)
Theorem	cleq2d 1112	Deduction from equality to equivalence of equalities.
|- (ph -> A = B)   =>   |- (ph -> (C = A <-> C = B))
Theorem	cleq12 1113	Equality relationship among 4 classes.
|- ((A = B /\ C = D) -> (A = C <-> B = D))
Theorem	cleq12i 1114	A useful inference for substituting definitions into an equality.
|- A = B   &   |- C = D   =>   |- (A = C <-> B = D)
Theorem	cleq12d 1115	A useful inference for substituting definitions into an equality.
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A = C <-> B = D))
Theorem	cleqan12d 1116	A useful inference for substituting definitions into an equality.
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ph /\ ps) -> (A = C <-> B = D))
Theorem	cleqan12rd 1117	A useful inference for substituting definitions into an equality.
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ps /\ ph) -> (A = C <-> B = D))
Theorem	cleqtr 1118	Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13.
|- ((A = B /\ B = C) -> A = C)
Theorem	eqtr 1119	An equality transitivity inference.
|- A = B   &   |- B = C   =>   |- A = C
Theorem	eqtr2 1120	An equality transitivity inference.
|- A = B   &   |- B = C   =>   |- C = A
Theorem	eqtr3 1121	An equality transitivity inference.
|- A = B   &   |- A = C   =>   |- B = C
Theorem	eqtr4 1122	An equality transitivity inference.
|- A = B   &   |- C = B   =>   |- A = C
Theorem	3eqtr 1123	An inference from three chained equalities.
|- A = B   &   |- B = C   &   |- C = D   =>   |- A = D
Theorem	3eqtr3 1124	An inference from three chained equalities.
|- A = B   &   |- A = C   &   |- B = D   =>   |- C = D
Theorem	3eqtr3r 1125	An inference from three chained equalities.
|- A = B   &   |- A = C   &   |- B = D   =>   |- D = C
Theorem	3eqtr4 1126	An inference from three chained equalities.
|- A = B   &   |- C = A   &   |- D = B   =>   |- C = D
Theorem	3eqtr4r 1127	An inference from three chained equalities.
|- A = B   &   |- C = A   &   |- D = B   =>   |- D = C
Theorem	eqtrd 1128	An equality transitivity deduction.
|- (ph -> A = B)   &   |- (ph -> B = C)   =>   |- (ph -> A = C)
Theorem	eqtr2d 1129	An equality transitivity deduction.
|- (ph -> A = B)   &   |- (ph -> B = C)   =>   |- (ph -> C = A)
Theorem	eqtr3d 1130	An equality transitivity equality deduction.
|- (ph -> A = B)   &   |- (ph -> A = C)   =>   |- (ph -> B = C)
Theorem	eqtr4d 1131	An equality transitivity equality deduction.
|- (ph -> A = B)   &   |- (ph -> C = B)   =>   |- (ph -> A = C)
Theorem	3eqtrd 1132	A deduction from three chained equalities.
|- (ph -> A = B)   &   |- (ph -> B = C)   &   |- (ph -> C = D)   =>   |- (ph -> A = D)
Theorem	3eqtr3d 1133	A deduction from three chained equalities.
|- (ph -> A = B)   &   |- (ph -> A = C)   &   |- (ph -> B = D)   =>   |- (ph -> C = D)
Theorem	3eqtr4d 1134	A deduction from three chained equalities.
|- (ph -> A = B)   &   |- (ph -> C = A)   &   |- (ph -> D = B)   =>   |- (ph -> C = D)
Theorem	3eqtr4rd 1135	A deduction from three chained equalities.
|- (ph -> A = B)   &   |- (ph -> C = A)   &   |- (ph -> D = B)   =>   |- (ph -> D = C)
Theorem	syl5eq 1136	An equality transitivity deduction.
|- (ph -> A = B)   &   |- C = A   =>   |- (ph -> C = B)
Theorem	syl5req 1137	An equality transitivity deduction.
|- (ph -> A = B)   &   |- C = A   =>   |- (ph -> B = C)
Theorem	syl5eqr 1138	An equality transitivity deduction.
|- (ph -> A = B)   &   |- A = C   =>   |- (ph -> C = B)
Theorem	syl5reqr 1139	An equality transitivity deduction.
|- (ph -> A = B)   &   |- A = C   =>   |- (ph -> B = C)
Theorem	syl6eq 1140	An equality transitivity deduction.
|- (ph -> A = B)   &   |- B = C   =>   |- (ph -> A = C)
Theorem	syl6req 1141	An equality transitivity deduction.
|- (ph -> A = B)   &   |- B = C   =>   |- (ph -> C = A)
Theorem	syl6eqr 1142	An equality transitivity deduction.
|- (ph -> A = B)   &   |- C = B   =>   |- (ph -> A = C)
Theorem	syl6reqr 1143	An equality transitivity deduction.
|- (ph -> A = B)   &   |- C = B   =>   |- (ph -> C = A)
Theorem	sylan9eq 1144	An equality transitivity deduction.
|- (ph -> A = B)   &   |- (ps -> B = C)   =>   |- ((ph /\ ps) -> A = C)
Theorem	sylan9eqr 1145	An equality transitivity deduction.
|- (ph -> A = B)   &   |- (ps -> B = C)   =>   |- ((ps /\ ph) -> A = C)
Theorem	3eqtr3g 1146	A chained equality inference, useful for converting from definitions.
|- (ph -> A = B)   &   |- A = C   &   |- B = D   =>   |- (ph -> C = D)
Theorem	3eqtr4g 1147	A chained equality inference, useful for converting to definitions.
|- (ph -> A = B)   &   |- C = A   &   |- D = B   =>   |- (ph -> C = D)
Theorem	cleq2tr 1148	A compound transitive inference for class equality.
|- (A = C -> D = F)   &   |- (B = D -> C = G)   =>   |- ((A = C /\ B = F) <-> (B = D /\ A = G))
Theorem	eleq1 1149	Equality implies equivalence of membership.
|- (A = B -> (A e. C <-> B e. C))
Theorem	eleq2 1150	Equality implies equivalence of membership.
|- (A = B -> (C e. A <-> C e. B))
Theorem	eleq12 1151	Equality implies equivalence of membership.
|- ((A = B /\ C = D) -> (A e. C <-> B e. D))
Theorem	eleq1i 1152	Inference from equality to equivalence of membership.
|- A = B   =>   |- (A e. C <-> B e. C)
Theorem	eleq2i 1153	Inference from equality to equivalence of membership.
|- A = B   =>   |- (C e. A <-> C e. B)
Theorem	eleq12i 1154	Inference from equality to equivalence of membership.
|- A = B   &   |- C = D   =>   |- (A e. C <-> B e. D)
Theorem	eleq1d 1155	Deduction from equality to equivalence of membership.
|- (ph -> A = B)   =>   |- (ph -> (A e. C <-> B e. C))
Theorem	eleq2d 1156	Deduction from equality to equivalence of membership.
|- (ph -> A = B)   =>   |- (ph -> (C e. A <-> C e. B))
Theorem	eleq12d 1157	Deduction from equality to equivalence of membership.
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A e. C <-> B e. D))
Theorem	eleq1a 1158	A transitive-type law relating membership and equality.
|- (A e. B -> (C = A -> C e. B))
Theorem	eqeltr 1159	Substitution of equal classes into membership relation.
|- A = B   &   |- B e. C   =>   |- A e. C
Theorem	eqeltrr 1160	Substitution of equal classes into membership relation.
|- A = B   &   |- A e. C   =>   |- B e. C
Theorem	eleqtr 1161	Substitution of equal classes into membership relation.
|- A e. B   &   |- B = C   =>   |- A e. C
Theorem	eleqtrr 1162	Substitution of equal classes into membership relation.
|- A e. B   &   |- C = B   =>   |- A e. C
Theorem	eqeltrd 1163	Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-02.)
|- (ph -> A = B)   &   |- (ph -> B e. C)   =>   |- (ph -> A e. C)
Theorem	eqeltrrd 1164	Deduction that substitutes equal classes into membership.
|- (ph -> A = B)   &   |- (ph -> A e. C)   =>   |- (ph -> B e. C)
Theorem	eleqtrd 1165	Deduction that substitutes equal classes into membership.
|- (ph -> A e. B)   &   |- (ph -> B = C)   =>   |- (ph -> A e. C)
Theorem	eleqtrrd 1166	Deduction that substitutes equal classes into membership.
|- (ph -> A e. B)   &   |- (ph -> C = B)   =>   |- (ph -> A e. C)
Theorem	cleqf 1167	Establish equality between classes, requiring only that x not be 'free' in A and B (but not necessarily absent from them).
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (A = B <-> A.x(x e. A <-> x e. B))
Theorem	clneq 1168	A way of showing two classes are not equal.
|- ((A e. C /\ -. B e. C) -> -. A = B)
Theorem	clneq2 1169	A way of showing two classes are not equal.
|- ((A e. B /\ -. A e. C) -> -. B = C)
Theorem	hblem 1170	Lemma for hbeq 1171 and hbel 1172.
|- (y e. A -> A.x y e. A)   =>   |- (z e. A -> A.x z e. A)
Theorem	hbeq 1171	If x is effectively bound in A and B, it is effectively bound in A = B.
|- (y e. A -> A.x y e. A)   &   |- (