mmtheorems16 - 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-10687

Statement List for Metamath Proof Explorer - 1501-1600 - Page 16 of 107

Type	Label	Description
Statement
Theorem	3eqtr3r 1501	An inference from three chained equalities.
|- A = B   &   |- A = C   &   |- B = D   =>   |- D = C
Theorem	3eqtr4 1502	An inference from three chained equalities.
|- A = B   &   |- C = A   &   |- D = B   =>   |- C = D
Theorem	3eqtr4r 1503	An inference from three chained equalities.
|- A = B   &   |- C = A   &   |- D = B   =>   |- D = C
Theorem	eqtrd 1504	An equality transitivity deduction.
|- (ph -> A = B)   &   |- (ph -> B = C)   =>   |- (ph -> A = C)
Theorem	eqtr2d 1505	An equality transitivity deduction.
|- (ph -> A = B)   &   |- (ph -> B = C)   =>   |- (ph -> C = A)
Theorem	eqtr3d 1506	An equality transitivity equality deduction.
|- (ph -> A = B)   &   |- (ph -> A = C)   =>   |- (ph -> B = C)
Theorem	eqtr4d 1507	An equality transitivity equality deduction.
|- (ph -> A = B)   &   |- (ph -> C = B)   =>   |- (ph -> A = C)
Theorem	3eqtrd 1508	A deduction from three chained equalities.
|- (ph -> A = B)   &   |- (ph -> B = C)   &   |- (ph -> C = D)   =>   |- (ph -> A = D)
Theorem	3eqtrrd 1509	A deduction from three chained equalities.
|- (ph -> A = B)   &   |- (ph -> B = C)   &   |- (ph -> C = D)   =>   |- (ph -> D = A)
Theorem	3eqtr2d 1510	A deduction from three chained equalities.
|- (ph -> A = B)   &   |- (ph -> C = B)   &   |- (ph -> C = D)   =>   |- (ph -> A = D)
Theorem	3eqtr2rd 1511	A deduction from three chained equalities.
|- (ph -> A = B)   &   |- (ph -> C = B)   &   |- (ph -> C = D)   =>   |- (ph -> D = A)
Theorem	3eqtr3d 1512	A deduction from three chained equalities.
|- (ph -> A = B)   &   |- (ph -> A = C)   &   |- (ph -> B = D)   =>   |- (ph -> C = D)
Theorem	3eqtr3rd 1513	A deduction from three chained equalities.
|- (ph -> A = B)   &   |- (ph -> A = C)   &   |- (ph -> B = D)   =>   |- (ph -> D = C)
Theorem	3eqtr4d 1514	A deduction from three chained equalities.
|- (ph -> A = B)   &   |- (ph -> C = A)   &   |- (ph -> D = B)   =>   |- (ph -> C = D)
Theorem	3eqtr4rd 1515	A deduction from three chained equalities.
|- (ph -> A = B)   &   |- (ph -> C = A)   &   |- (ph -> D = B)   =>   |- (ph -> D = C)
Theorem	syl5eq 1516	An equality transitivity deduction.
|- (ph -> A = B)   &   |- C = A   =>   |- (ph -> C = B)
Theorem	syl5req 1517	An equality transitivity deduction.
|- (ph -> A = B)   &   |- C = A   =>   |- (ph -> B = C)
Theorem	syl5eqr 1518	An equality transitivity deduction.
|- (ph -> A = B)   &   |- A = C   =>   |- (ph -> C = B)
Theorem	syl5reqr 1519	An equality transitivity deduction.
|- (ph -> A = B)   &   |- A = C   =>   |- (ph -> B = C)
Theorem	syl6eq 1520	An equality transitivity deduction.
|- (ph -> A = B)   &   |- B = C   =>   |- (ph -> A = C)
Theorem	syl6req 1521	An equality transitivity deduction.
|- (ph -> A = B)   &   |- B = C   =>   |- (ph -> C = A)
Theorem	syl6eqr 1522	An equality transitivity deduction.
|- (ph -> A = B)   &   |- C = B   =>   |- (ph -> A = C)
Theorem	syl6reqr 1523	An equality transitivity deduction.
|- (ph -> A = B)   &   |- C = B   =>   |- (ph -> C = A)
Theorem	sylan9eq 1524	An equality transitivity deduction.
|- (ph -> A = B)   &   |- (ps -> B = C)   =>   |- ((ph /\ ps) -> A = C)
Theorem	sylan9req 1525	An equality transitivity deduction.
|- (ph -> B = A)   &   |- (ps -> B = C)   =>   |- ((ph /\ ps) -> A = C)
Theorem	sylan9eqr 1526	An equality transitivity deduction.
|- (ph -> A = B)   &   |- (ps -> B = C)   =>   |- ((ps /\ ph) -> A = C)
Theorem	3eqtr3g 1527	A chained equality inference, useful for converting from definitions.
|- (ph -> A = B)   &   |- A = C   &   |- B = D   =>   |- (ph -> C = D)
Theorem	3eqtr4g 1528	A chained equality inference, useful for converting to definitions.
|- (ph -> A = B)   &   |- C = A   &   |- D = B   =>   |- (ph -> C = D)
Theorem	3eqtr4a 1529	A chained equality inference, useful for converting to definitions.
|- A = B   &   |- (ph -> C = A)   &   |- (ph -> D = B)   =>   |- (ph -> C = D)
Theorem	eq2tr 1530	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 1531	Equality implies equivalence of membership.
|- (A = B -> (A e. C <-> B e. C))
Theorem	eleq2 1532	Equality implies equivalence of membership.
|- (A = B -> (C e. A <-> C e. B))
Theorem	eleq12 1533	Equality implies equivalence of membership.
|- ((A = B /\ C = D) -> (A e. C <-> B e. D))
Theorem	eleq1i 1534	Inference from equality to equivalence of membership.
|- A = B   =>   |- (A e. C <-> B e. C)
Theorem	eleq2i 1535	Inference from equality to equivalence of membership.
|- A = B   =>   |- (C e. A <-> C e. B)
Theorem	eleq12i 1536	Inference from equality to equivalence of membership.
|- A = B   &   |- C = D   =>   |- (A e. C <-> B e. D)
Theorem	eleq1d 1537	Deduction from equality to equivalence of membership.
|- (ph -> A = B)   =>   |- (ph -> (A e. C <-> B e. C))
Theorem	eleq2d 1538	Deduction from equality to equivalence of membership.
|- (ph -> A = B)   =>   |- (ph -> (C e. A <-> C e. B))
Theorem	eleq12d 1539	Deduction from equality to equivalence of membership.
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A e. C <-> B e. D))
Theorem	eleq1a 1540	A transitive-type law relating membership and equality.
|- (A e. B -> (C = A -> C e. B))
Theorem	eqeltr 1541	Substitution of equal classes into membership relation.
|- A = B   &   |- B e. C   =>   |- A e. C
Theorem	eqeltrr 1542	Substitution of equal classes into membership relation.
|- A = B   &   |- A e. C   =>   |- B e. C
Theorem	eleqtr 1543	Substitution of equal classes into membership relation.
|- A e. B   &   |- B = C   =>   |- A e. C
Theorem	eleqtrr 1544	Substitution of equal classes into membership relation.
|- A e. B   &   |- C = B   =>   |- A e. C
Theorem	eqeltrd 1545	Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
|- (ph -> A = B)   &   |- (ph -> B e. C)   =>   |- (ph -> A e. C)
Theorem	eqeltrrd 1546	Deduction that substitutes equal classes into membership.
|- (ph -> A = B)   &   |- (ph -> A e. C)   =>   |- (ph -> B e. C)
Theorem	eleqtrd 1547	Deduction that substitutes equal classes into membership.
|- (ph -> A e. B)   &   |- (ph -> B = C)   =>   |- (ph -> A e. C)
Theorem	eleqtrrd 1548	Deduction that substitutes equal classes into membership.
|- (ph -> A e. B)   &   |- (ph -> C = B)   =>   |- (ph -> A e. C)
Theorem	syl5eqel 1549	A membership and equality inference.
|- (ph -> A e. B)   &   |- C = A   =>   |- (ph -> C e. B)
Theorem	syl5eqelr 1550	A membership and equality inference.
|- (ph -> A e. B)   &   |- A = C   =>   |- (ph -> C e. B)
Theorem	syl5eleq 1551	A membership and equality inference.
|- (ph -> A = B)   &   |- C e. A   =>   |- (ph -> C e. B)
Theorem	syl5eleqr 1552	A membership and equality inference.
|- (ph -> B = A)   &   |- C e. A   =>   |- (ph -> C e. B)
Theorem	syl6eqel 1553	A membership and equality inference.
|- (ph -> A = B)   &   |- B e. C   =>   |- (ph -> A e. C)
Theorem	syl6eqelr 1554	A membership and equality inference.
|- (ph -> B = A)   &   |- B e. C   =>   |- (ph -> A e. C)
Theorem	syl6eleq 1555	A membership and equality inference.
|- (ph -> A e. B)   &   |- B = C   =>   |- (ph -> A e. C)
Theorem	syl6eleqr 1556	A membership and equality inference.
|- (ph -> A e. B)   &   |- C = B   =>   |- (ph -> A e. C)
Theorem	cleqf 1557	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions.
|- (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	nelneq 1558	A way of showing two classes are not equal.
|- ((A e. C /\ -. B e. C) -> -. A = B)
Theorem	nelneq2 1559	A way of showing two classes are not equal.
|- ((A e. B /\ -. A e. C) -> -. B = C)
Theorem	hbxfr 1560	A utility lemma to transfer a bound-variable hypothesis builder into a definition.
|- A = B   &   |- (y e. B -> A.x y e. B)   =>   |- (y e. A -> A.x y e. A)
Theorem	hblem 1561	Lemma for hbeq 1562 and hbel 1563.
Theorem	hbeq 1562	If x is effectively bound in A and B, it is effectively bound in A = B.
|- (y e. A -> A.x y e. A)   &   |-