mmtheorems17 - 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-10670

Statement List for Metamath Proof Explorer - 1601-1700 - Page 17 of 107

Type	Label	Description
Statement
Theorem	necon3bd 1601	Contrapositive law deduction for inequality.
|- (ph -> (A = B -> ps))   =>   |- (ph -> (-. ps -> A =/= B))
Theorem	necon3d 1602	Contrapositive law deduction for inequality.
|- (ph -> (A = B -> C = D))   =>   |- (ph -> (C =/= D -> A =/= B))
Theorem	necon3i 1603	Contrapositive inference for inequality.
|- (A = B -> C = D)   =>   |- (C =/= D -> A =/= B)
Theorem	necon3ai 1604	Contrapositive inference for inequality.
|- (ph -> A = B)   =>   |- (A =/= B -> -. ph)
Theorem	necon3bi 1605	Contrapositive inference for inequality.
|- (A = B -> ph)   =>   |- (-. ph -> A =/= B)
Theorem	necon1ai 1606	Contrapositive inference for inequality.
|- (-. ph -> A = B)   =>   |- (A =/= B -> ph)
Theorem	necon1bi 1607	Contrapositive inference for inequality.
|- (A =/= B -> ph)   =>   |- (-. ph -> A = B)
Theorem	necon1i 1608	Contrapositive inference for inequality.
|- (A =/= B -> C = D)   =>   |- (C =/= D -> A = B)
Theorem	necon2ai 1609	Contrapositive inference for inequality.
|- (A = B -> -. ph)   =>   |- (ph -> A =/= B)
Theorem	necon2bi 1610	Contrapositive inference for inequality.
|- (ph -> A =/= B)   =>   |- (A = B -> -. ph)
Theorem	necon2i 1611	Contrapositive inference for inequality.
|- (A = B -> C =/= D)   =>   |- (C = D -> A =/= B)
Theorem	necon2ad 1612	Contrapositive inference for inequality.
|- (ph -> (A = B -> -. ps))   =>   |- (ph -> (ps -> A =/= B))
Theorem	necon2bd 1613	Contrapositive inference for inequality.
|- (ph -> (ps -> A =/= B))   =>   |- (ph -> (A = B -> -. ps))
Theorem	necon1abii 1614	Contrapositive inference for inequality.
|- (-. ph <-> A = B)   =>   |- (A =/= B <-> ph)
Theorem	necon1bbii 1615	Contrapositive inference for inequality.
|- (A =/= B <-> ph)   =>   |- (-. ph <-> A = B)
Theorem	necon1abid 1616	Contrapositive deduction for inequality.
|- (ph -> (-. ps <-> A = B))   =>   |- (ph -> (A =/= B <-> ps))
Theorem	necon1bbid 1617	Contrapositive inference for inequality.
|- (ph -> (A =/= B <-> ps))   =>   |- (ph -> (-. ps <-> A = B))
Theorem	necon2abii 1618	Contrapositive inference for inequality.
|- (A = B <-> -. ph)   =>   |- (ph <-> A =/= B)
Theorem	necon2bbii 1619	Contrapositive inference for inequality.
|- (ph <-> A =/= B)   =>   |- (A = B <-> -. ph)
Theorem	necon2abid 1620	Contrapositive deduction for inequality.
|- (ph -> (A = B <-> -. ps))   =>   |- (ph -> (ps <-> A =/= B))
Theorem	necon2bbid 1621	Contrapositive deduction for inequality.
|- (ph -> (ps <-> A =/= B))   =>   |- (ph -> (A = B <-> -. ps))
Theorem	necon4ai 1622	Contrapositive inference for inequality.
|- (A =/= B -> -. ph)   =>   |- (ph -> A = B)
Theorem	necon4i 1623	Contrapositive inference for inequality.
|- (A =/= B -> C =/= D)   =>   |- (C = D -> A = B)
Theorem	necon4ad 1624	Contrapositive inference for inequality.
|- (ph -> (A =/= B -> -. ps))   =>   |- (ph -> (ps -> A = B))
Theorem	necon4bd 1625	Contrapositive inference for inequality.
|- (ph -> (-. ps -> A =/= B))   =>   |- (ph -> (A = B -> ps))
Theorem	necon4d 1626	Contrapositive inference for inequality.
|- (ph -> (A =/= B -> C =/= D))   =>   |- (ph -> (C = D -> A = B))
Theorem	necon4abid 1627	Contrapositive law deduction for inequality.
|- (ph -> (A =/= B <-> -. ps))   =>   |- (ph -> (A = B <-> ps))
Theorem	necon4bid 1628	Contrapositive law deduction for inequality.
|- (ph -> (A =/= B <-> C =/= D))   =>   |- (ph -> (A = B <-> C = D))
Theorem	necon1ad 1629	Contrapositive deduction for inequality.
|- (ph -> (-. ps -> A = B))   =>   |- (ph -> (A =/= B -> ps))
Theorem	necon1bd 1630	Contrapositive deduction for inequality.
|- (ph -> (A =/= B -> ps))   =>   |- (ph -> (-. ps -> A = B))
Theorem	pm2.61ne 1631	Deduction eliminating an inequality in an antecedent.
|- (A = B -> (ps <-> ch))   &   |- ((ph /\ A =/= B) -> ps)   &   |- (ph -> ch)   =>   |- (ph -> ps)
Theorem	pm2.61ine 1632	Inference eliminating an inequality in an antecedent.
|- (A = B -> ph)   &   |- (A =/= B -> ph)   =>   |- ph
Theorem	pm2.61dne 1633	Deduction eliminating an inequality in an antecedent.
|- (ph -> (A = B -> ps))   &   |- (ph -> (A =/= B -> ps))   =>   |- (ph -> ps)
Theorem	necom 1634	Commutation of inequality.
|- (A =/= B <-> B =/= A)
Theorem	necomd 1635	Deduction from commutative law for inequality.
|- (ph -> A =/= B)   =>   |- (ph -> B =/= A)
Theorem	neor 1636	Logical OR with an equality.
|- ((A = B \/ ps) <-> (A =/= B -> ps))
Theorem	neanior 1637	A DeMorgan's law for inequality.
|- ((A =/= B /\ C =/= D) <-> -. (A = B \/ C = D))
Theorem	neorian 1638	A DeMorgan's law for inequality.
|- ((A =/= B \/ C =/= D) <-> -. (A = B /\ C = D))
Theorem	nemtbir 1639	An inference from an inequality, related to modus tollens.
|- A =/= B   &   |- (ph <-> A = B)   =>   |- -. ph
Theorem	neleq1 1640	Equality theorem for negated membership.
|- (A = B -> (A e/ C <-> B e/ C))
Theorem	neleq2 1641	Equality theorem for negated membership.
|- (A = B -> (C e/ A <-> C e/ B))
Theorem	hbne 1642	Bound-variable hypothesis builder for inequality.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (A =/= B -> A.x A =/= B)
Restricted quantification
Syntax	wral 1643	Extend wff notation to include restricted universal quantification.
wff A.x e. A ph
Syntax	wrex 1644	Extend wff notation to include restricted existential quantification.
wff E.x e. A ph
Syntax	wreu 1645	Extend wff notation to include restricted existential uniqueness.
wff E!x e. A ph
Syntax	crab 1646	Extend class notation to include the restricted class abstraction (class builder).
class {x e. A | ph}
Definition	df-ral 1647	Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22.
|- (A.x e. A ph <-> A.x(x e. A -> ph))
Definition	df-rex 1648	Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22.
|- (E.x e. A ph <-> E.x(x e. A /\ ph))
Definition	df-reu 1649	Define restricted existential uniqueness.
|- (E!x e. A ph <-> E!x(x e. A /\ ph))
Definition	df-rab 1650	Define a restricted class abstraction (class builder), which is the class of all x in A such that ph is true. Definition of [TakeutiZaring] p. 20.
|- {x e. A | ph} = {x | (x e. A /\ ph)}
Theorem	ralnex 1651	Relationship between restricted universal and existential quantifiers.
|- (A.x e. A -. ph <-> -. E.x e. A ph)
Theorem	rexnal 1652	Relationship between restricted universal and existential quantifiers.
|- (E.x e. A -. ph <-> -. A.x e. A ph)
Theorem	dfral2 1653	Relationship between restricted universal and existential quantifiers.
|- (A.x e. A ph <-> -. E.x e. A -. ph)
Theorem	dfrex2 1654	Relationship between restricted universal and existential quantifiers.
|- (E.x e. A ph <-> -. A.x e. A -. ph)
Theorem	ralbida 1655	Formula-building rule for restricted universal quantifier (deduction rule).
|- (ph -> A.xph)   &   |- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Theorem	rexbida 1656	Formula-building rule for restricted existential quantifier (deduction rule).
|- (ph -> A.xph)   &   |- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (E.x e. A ps <-> E.x e. A ch))
Theorem	ralbidva 1657	Formula-building rule for restricted universal quantifier (deduction rule).
|- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Theorem	rexbidva 1658	Formula-building rule for restricted existential quantifier (deduction rule).
|- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (E.x e. A ps <-> E.x e. A ch))
Theorem	ralbid 1659	Formula-building rule for restricted universal quantifier (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Theorem	rexbid 1660	Formula-building rule for restricted existential quantifier (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (E.x e. A ps <-> E.x e. A ch))
Theorem	ralbidv 1661	Formula-building rule for restricted universal quantifier (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Theorem	rexbidv 1662	Formula-building rule for restricted existential quantifier (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.x e. A ps <-> E.x e. A ch))
Theorem	ralbidv2 1663	Formula-building rule for restricted universal quantifier (deduction rule).
|- (ph -> ((x e. A -> ps) <-> (x e. B -> ch)))   =>   |- (ph -> (A.x e. A ps <-> A.x e. B ch))
Theorem	rexbidv2 1664	Formula-building rule for restricted existential quantifier (deduction rule).
|- (ph -> ((x e. A /\ ps) <-> (x e. B /\ ch)))   =>   |- (ph -> (E.x e. A ps <-> E.x e. B ch))
Theorem	ralbii 1665	Inference adding restricted universal quantifier to both sides of an equivalence.
|-