Metamath Proof Explorer

Home	Metamath Proof Explorer	< Previous Next >
		Browser slow? Try the Unicode version.

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

Color key:

Metamath Proof Explorer (1-4957)

Hilbert Space Explorer (4958-5787)

**Statement List for Metamath Proof Explorer -** 1501-1600 - Page 16 of 58
Type	Label	Description
Statement

Theorem	hbss 1501	If is not free in and , it is not free in .


Theorem	ssel 1502	Membership relationships follow from a subclass relationship.


Theorem	ssel2 1503	Membership relationships follow from a subclass relationship.
$/\$

Theorem	sseli 1504	Membership inference from subclass relationship.


Theorem	sselii 1505	Membership inference from subclass relationship.


Theorem	sseld 1506	Membership deduction from subclass relationship.


Theorem	sseldd 1507	Membership inference from subclass relationship.


Theorem	ssriv 1508	Inference rule based on subclass definition.


Theorem	ssrdv 1509	Deduction rule based on subclass definition.


Theorem	sstr2 1510	Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17.


Theorem	sstr 1511	Transitivity of subclasses. Theorem 6 of [Suppes] p. 23.
$/\$

Theorem	sstri 1512	Subclass transitivity inference.


Theorem	sstrd 1513	Subclass transitivity deduction.


Theorem	sylan9ss 1514	A subclass transitivity deduction.
$/\$

Theorem	sylan9ssr 1515	A subclass transitivity deduction.
$/\$

Theorem	eqss 1516	The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22.
$/\$

Theorem	eqssi 1517	Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22.


Theorem	eqssd 1518	Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22.


Theorem	ssid 1519	Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18.


Theorem	ssv 1520	Any class is a subclass of the universal class.


Theorem	sseq1 1521	Equality theorem for subclasses.


Theorem	sseq2 1522	Equality theorem for the subclass relationship.


Theorem	sseq12 1523	Equality theorem for the subclass relationship.
$/\$

Theorem	sseq1i 1524	An equality inference for the subclass relationship.


Theorem	sseq2i 1525	An equality inference for the subclass relationship.


Theorem	sseq12i 1526	An equality inference for the subclass relationship.


Theorem	sseq1d 1527	An equality deduction for the subclass relationship.


Theorem	sseq2d 1528	An equality deduction for the subclass relationship.


Theorem	sseq12d 1529	An equality deduction for the subclass relationship.


Theorem	eqsstr 1530	Substitution of equality into a subclass relationship.


Theorem	eqsstr3 1531	Substitution of equality into a subclass relationship.


Theorem	sseqtr 1532	Substitution of equality into a subclass relationship.


Theorem	sseqtr4 1533	Substitution of equality into a subclass relationship.


Theorem	eqsstrd 1534	Substitution of equality into a subclass relationship.


Theorem	eqsstr3d 1535	Substitution of equality into a subclass relationship.


Theorem	sseqtrd 1536	Substitution of equality into a subclass relationship.


Theorem	sseqtr4d 1537	Substitution of equality into a subclass relationship.


Theorem	3sstr3 1538	Substitution of equality in both sides of a subclass relationship.


Theorem	3sstr4 1539	Substitution of equality in both sides of a subclass relationship.


Theorem	3sstr3g 1540	Substitution of equality into both sides of a subclass relationship.


Theorem	3sstr4g 1541	Substitution of equality into both sides of a subclass relationship.


Theorem	3sstr3d 1542	Substitution of equality into both sides of a subclass relationship.


Theorem	3sstr4d 1543	Substitution of equality into both sides of a subclass relationship.


Theorem	syl5ss 1544	A chained subclass and equality deduction.


Theorem	syl5ssr 1545	A chained subclass and equality deduction.


Theorem	syl6ss 1546	A chained subclass and equality deduction.


Theorem	syl6ssr 1547	A chained subclass and equality deduction.


Theorem	eqimss 1548	Equality implies the subclass relation.


Theorem	eqimss2 1549	Equality implies the subclass relation.


Theorem	nss 1550	Negation of subclass relationship. Exercise 13 of [TakeutiZaring] p. 18.
$/\$

Theorem	ss2ab 1551	Equivalence of abstraction subclass and implication.


Theorem	ss2abi 1552	Inference of abstraction subclass from implication.


Theorem	ss2rab 1553	Equivalence of restricted abstraction subclass and implication.


Theorem	ss2rabi 1554	Inference of restricted abstraction subclass from implication.


Theorem	ssab 1555	Restriction of class abstraction creates subclass.
$/\$

Theorem	ssrab 1556	Restriction of class abstraction creates subclass.


Theorem	dfpss2 1557	Alternate definition of proper subclass.
$/\$

Theorem	dfpss3 1558	Alternate definition of proper subclass.
$/\$

Theorem	psseq1 1559	Equality theorem for proper subclass.


Theorem	psseq2 1560	Equality theorem for proper subclass.


Theorem	psseq1i 1561	An equality inference for the proper subclass relationship.


Theorem	psseq2i 1562	An equality inference for the proper subclass relationship.


Theorem	psseq12i 1563	An equality inference for the proper subclass relationship.


Theorem	psseq1d 1564	An equality deduction for the proper subclass relationship.


Theorem	psseq2d 1565	An equality deduction for the proper subclass relationship.


Theorem	psseq12d 1566	An equality deduction for the proper subclass relationship.


Theorem	pssss 1567	A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23.


Theorem	pssssd 1568	Deduce subclass from proper subclass.


Theorem	sspss 1569	Subclass in terms of proper subclass.
$\/$

Theorem	pssirr 1570	Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23.


Theorem	pssn2lp 1571	Proper subclass has no 2-cycle loops. Compare Theorem 8 of [Suppes] p. 23.
$/\$

Theorem	sspsstri 1572	Two ways of stating trichotomy with respect to inclusion.
$\/$ $\/$ $\/$

Theorem	ssnpss 1573	Partial trichotomy law for subclasses.


Theorem	psstr 1574	Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23.
$/\$

Theorem	sspsstr 1575	Transitive law for subclass and proper subclass.
$/\$

Theorem	psssstr 1576	Transitive law for subclass and proper subclass.
$/\$

Theorem	reuss 1577	Restriction of uniqueness to a smaller subclass.
$/\$ $/\$

Theorem	reupick 1578	Restricted uniqueness "picks" a member of a subclass.
$/\$