Metamath Proof Explorer - mmtheorems16

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 - 1501-1600 - Page 16 of 58

Type	Label	Description
Statement
Theorem	hbss 1501	If x is not free in A and B, it is not free in A ⊆ B.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (A ⊆ B → ∀x A ⊆ B)
Theorem	ssel 1502	Membership relationships follow from a subclass relationship.
⊢ (A ⊆ B → (C ∈ A → C ∈ B))
Theorem	ssel2 1503	Membership relationships follow from a subclass relationship.
⊢ ((A ⊆ B ∧ C ∈ A) → C ∈ B)
Theorem	sseli 1504	Membership inference from subclass relationship.
⊢ A ⊆ B    ⇒   ⊢ (C ∈ A → C ∈ B)
Theorem	sselii 1505	Membership inference from subclass relationship.
⊢ A ⊆ B    &   ⊢ C ∈ A    ⇒   ⊢ C ∈ B
Theorem	sseld 1506	Membership deduction from subclass relationship.
⊢ (φ → A ⊆ B)    ⇒   ⊢ (φ → (C ∈ A → C ∈ B))
Theorem	sseldd 1507	Membership inference from subclass relationship.
⊢ (φ → A ⊆ B)    &   ⊢ (φ → C ∈ A)    ⇒   ⊢ (φ → C ∈ B)
Theorem	ssriv 1508	Inference rule based on subclass definition.
⊢ (x ∈ A → x ∈ B)    ⇒   ⊢ A ⊆ B
Theorem	ssrdv 1509	Deduction rule based on subclass definition.
⊢ (φ → (x ∈ A → x ∈ B))    ⇒   ⊢ (φ → A ⊆ B)
Theorem	sstr2 1510	Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17.
⊢ (A ⊆ B → (B ⊆ C → A ⊆ C))
Theorem	sstr 1511	Transitivity of subclasses. Theorem 6 of [Suppes] p. 23.
⊢ ((A ⊆ B ∧ B ⊆ C) → A ⊆ C)
Theorem	sstri 1512	Subclass transitivity inference.
⊢ A ⊆ B    &   ⊢ B ⊆ C    ⇒   ⊢ A ⊆ C
Theorem	sstrd 1513	Subclass transitivity deduction.
⊢ (φ → A ⊆ B)    &   ⊢ (φ → B ⊆ C)    ⇒   ⊢ (φ → A ⊆ C)
Theorem	sylan9ss 1514	A subclass transitivity deduction.
⊢ (φ → A ⊆ B)    &   ⊢ (ψ → B ⊆ C)    ⇒   ⊢ ((φ ∧ ψ) → A ⊆ C)
Theorem	sylan9ssr 1515	A subclass transitivity deduction.
⊢ (φ → A ⊆ B)    &   ⊢ (ψ → B ⊆ C)    ⇒   ⊢ ((ψ ∧ φ) → A ⊆ C)
Theorem	eqss 1516	The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22.
⊢ (A = B ↔ (A ⊆ B ∧ B ⊆ A))
Theorem	eqssi 1517	Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22.
⊢ A ⊆ B    &   ⊢ B ⊆ A    ⇒   ⊢ A = B
Theorem	eqssd 1518	Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22.
⊢ (φ → A ⊆ B)    &   ⊢ (φ → B ⊆ A)    ⇒   ⊢ (φ → A = B)
Theorem	ssid 1519	Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18.
⊢ A ⊆ A
Theorem	ssv 1520	Any class is a subclass of the universal class.
⊢ A ⊆ V
Theorem	sseq1 1521	Equality theorem for subclasses.
⊢ (A = B → (A ⊆ C ↔ B ⊆ C))
Theorem	sseq2 1522	Equality theorem for the subclass relationship.
⊢ (A = B → (C ⊆ A ↔ C ⊆ B))
Theorem	sseq12 1523	Equality theorem for the subclass relationship.
⊢ ((A = B ∧ C = D) → (A ⊆ C ↔ B ⊆ D))
Theorem	sseq1i 1524	An equality inference for the subclass relationship.
⊢ A = B    ⇒   ⊢ (A ⊆ C ↔ B ⊆ C)
Theorem	sseq2i 1525	An equality inference for the subclass relationship.
⊢ A = B    ⇒   ⊢ (C ⊆ A ↔ C ⊆ B)
Theorem	sseq12i 1526	An equality inference for the subclass relationship.
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A ⊆ C ↔ B ⊆ D)
Theorem	sseq1d 1527	An equality deduction for the subclass relationship.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ⊆ C ↔ B ⊆ C))
Theorem	sseq2d 1528	An equality deduction for the subclass relationship.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ⊆ A ↔ C ⊆ B))
Theorem	sseq12d 1529	An equality deduction for the subclass relationship.
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A ⊆ C ↔ B ⊆ D))
Theorem	eqsstr 1530	Substitution of equality into a subclass relationship.
⊢ A = B    &   ⊢ B ⊆ C    ⇒   ⊢ A ⊆ C
Theorem	eqsstr3 1531	Substitution of equality into a subclass relationship.
⊢ B = A    &   ⊢ B ⊆ C    ⇒   ⊢ A ⊆ C
Theorem	sseqtr 1532	Substitution of equality into a subclass relationship.
⊢ A ⊆ B    &   ⊢ B = C    ⇒   ⊢ A ⊆ C
Theorem	sseqtr4 1533	Substitution of equality into a subclass relationship.
⊢ A ⊆ B    &   ⊢ C = B    ⇒   ⊢ A ⊆ C
Theorem	eqsstrd 1534	Substitution of equality into a subclass relationship.
⊢ (φ → A = B)    &   ⊢ (φ → B ⊆ C)    ⇒   ⊢ (φ → A ⊆ C)
Theorem	eqsstr3d 1535	Substitution of equality into a subclass relationship.
⊢ (φ → B = A)    &   ⊢ (φ → B ⊆ C)    ⇒   ⊢ (φ → A ⊆ C)
Theorem	sseqtrd 1536	Substitution of equality into a subclass relationship.
⊢ (φ → A ⊆ B)    &   ⊢ (φ → B = C)    ⇒   ⊢ (φ → A ⊆ C)
Theorem	sseqtr4d 1537	Substitution of equality into a subclass relationship.
⊢ (φ → A ⊆ B)    &   ⊢ (φ → C = B)    ⇒   ⊢ (φ → A ⊆ C)
Theorem	3sstr3 1538	Substitution of equality in both sides of a subclass relationship.
⊢ A ⊆ B    &   ⊢ A = C    &   ⊢ B = D    ⇒   ⊢ C ⊆ D
Theorem	3sstr4 1539	Substitution of equality in both sides of a subclass relationship.
⊢ A ⊆ B    &   ⊢ C = A    &   ⊢ D = B    ⇒   ⊢ C ⊆ D
Theorem	3sstr3g 1540	Substitution of equality into both sides of a subclass relationship.
⊢ (φ → A ⊆ B)    &   ⊢ A = C    &   ⊢ B = D    ⇒   ⊢ (φ → C ⊆ D)
Theorem	3sstr4g 1541	Substitution of equality into both sides of a subclass relationship.
⊢ (φ → A ⊆ B)    &   ⊢ C = A    &   ⊢ D = B    ⇒   ⊢ (φ → C ⊆ D)
Theorem	3sstr3d 1542	Substitution of equality into both sides of a subclass relationship.
⊢ (φ → A ⊆ B)    &   ⊢ (φ → A = C)    &   ⊢ (φ → B = D)    ⇒   ⊢ (φ → C ⊆ D)
Theorem	3sstr4d 1543	Substitution of equality into both sides of a subclass relationship.
⊢ (φ → A ⊆ B)    &   ⊢ (φ → C = A)    &   ⊢ (φ → D = B)    ⇒   ⊢ (φ → C ⊆ D)
Theorem	syl5ss 1544	A chained subclass and equality deduction.
⊢ (φ → A ⊆ B)    &   ⊢ C = A    ⇒   ⊢ (φ → C ⊆ B)
Theorem	syl5ssr 1545	A chained subclass and equality deduction.
⊢ (φ → A ⊆ B)    &   ⊢ A = C    ⇒   ⊢ (φ → C ⊆ B)
Theorem	syl6ss 1546	A chained subclass and equality deduction.
⊢ (φ → A ⊆ B)    &   ⊢ B = C    ⇒   ⊢ (φ → A ⊆ C)
Theorem	syl6ssr 1547	A chained subclass and equality deduction.
⊢ (φ → A ⊆ B)    &   ⊢ C = B    ⇒   ⊢ (φ → A ⊆ C)
Theorem	eqimss 1548	Equality implies the subclass relation.
⊢ (A = B → A ⊆ B)
Theorem	eqimss2 1549	Equality implies the subclass relation.
⊢ (B = A → A ⊆ B)
Theorem	nss 1550	Negation of subclass relationship. Exercise 13 of [TakeutiZaring] p. 18.
⊢ (¬ A ⊆ B ↔ ∃x(x ∈ A ∧ ¬ x ∈ B))
Theorem	ss2ab 1551	Equivalence of abstraction subclass and implication.
⊢ ({x∣φ} ⊆ {x∣ψ} ↔ ∀x(φ → ψ))
Theorem	ss2abi 1552	Inference of abstraction subclass from implication.
⊢ (φ → ψ)    ⇒   ⊢ {x∣φ} ⊆ {x∣ψ}
Theorem	ss2rab 1553	Equivalence of restricted abstraction subclass and implication.
⊢ ({x ∈ A∣φ} ⊆ {x ∈ A∣ψ} ↔ ∀x ∈ A (φ → ψ))
Theorem	ss2rabi 1554	Inference of restricted abstraction subclass from implication.
⊢ (x ∈ A → (φ → ψ))    ⇒   ⊢ {x ∈ A∣φ} ⊆ {x ∈ A∣ψ}
Theorem	ssab 1555	Restriction of class abstraction creates subclass.
⊢ {x∣(x ∈ A ∧ φ)} ⊆ A
Theorem	ssrab 1556	Restriction of class abstraction creates subclass.
⊢ {x ∈ A∣φ} ⊆ A
Theorem	dfpss2 1557	Alternate definition of proper subclass.
⊢ (A ⊂ B ↔ (A ⊆ B ∧ ¬ A = B))
Theorem	dfpss3 1558	Alternate definition of proper subclass.
⊢ (A ⊂ B ↔ (A ⊆ B ∧ ¬ B ⊆ A))
Theorem	psseq1 1559	Equality theorem for proper subclass.
⊢ (A = B → (A ⊂ C ↔ B ⊂ C))
Theorem	psseq2 1560	Equality theorem for proper subclass.
⊢ (A = B → (C ⊂ A ↔ C ⊂ B))
Theorem	psseq1i 1561	An equality inference for the proper subclass relationship.
⊢ A = B    ⇒   ⊢ (A ⊂ C ↔ B ⊂ C)
Theorem	psseq2i 1562	An equality inference for the proper subclass relationship.
⊢ A = B    ⇒   ⊢ (C ⊂ A ↔ C ⊂ B)
Theorem	psseq12i 1563	An equality inference for the proper subclass relationship.
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A ⊂ C ↔ B ⊂ D)
Theorem	psseq1d 1564	An equality deduction for the proper subclass relationship.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ⊂ C ↔ B ⊂ C))
Theorem	psseq2d 1565	An equality deduction for the proper subclass relationship.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ⊂ A ↔ C ⊂ B))
Theorem	psseq12d 1566	An equality deduction for the proper subclass relationship.
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A ⊂ C ↔ B ⊂ D))
Theorem	pssss 1567	A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23.
⊢ (A ⊂ B → A ⊆ B)
Theorem	pssssd 1568	Deduce subclass from proper subclass.
⊢ (φ → A ⊂ B)    ⇒   ⊢ (φ → A ⊆ B)
Theorem	sspss 1569	Subclass in terms of proper subclass.
⊢ (A ⊆ B ↔ (A ⊂ B ∨ A = B))
Theorem	pssirr 1570	Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23.
⊢ ¬ A ⊂ A
Theorem	pssn2lp 1571	Proper subclass has no 2-cycle loops. Compare Theorem 8 of [Suppes] p. 23.
⊢ ¬ (A ⊂ B ∧ B ⊂ A)
Theorem	sspsstri 1572	Two ways of stating trichotomy with respect to inclusion.
⊢ ((A ⊆ B ∨ B ⊆ A) ↔ (A ⊂ B ∨ A = B ∨ B ⊂ A))
Theorem	ssnpss 1573	Partial trichotomy law for subclasses.
⊢ (A ⊆ B → ¬ B ⊂ A)
Theorem	psstr 1574	Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23.
⊢ ((A ⊂ B ∧ B ⊂ C) → A ⊂ C)
Theorem	sspsstr 1575	Transitive law for subclass and proper subclass.
⊢ ((A ⊆ B ∧ B ⊂ C) → A ⊂ C)
Theorem	psssstr 1576	Transitive law for subclass and proper subclass.
⊢ ((A ⊂ B ∧ B ⊆ C) → A ⊂ C)
Theorem	reuss 1577	Restriction of uniqueness to a smaller subclass.
⊢ ((A ⊆ B ∧ (∃x ∈ A φ ∧ ∃!x ∈ B φ)) → ∃!x ∈ A φ)
Theorem	reupick 1578	Restricted uniqueness "picks" a member of a subclass.
⊢ (((A ⊆ B ∧ (∃x ∈ A φ ∧ ∃!x ∈ B φ)) ∧ φ) → (x ∈ A ↔ x ∈ B))
Theorem	reuxfr2 1579	Transfer existential uniqueness from a variable x to another variable y contained in expression A.
⊢ (y ∈ B → A ∈ B)    &   ⊢ (x ∈ B → ∃*y(y ∈ B ∧ x = A))    ⇒   ⊢ (∃!x ∈ B ∃y ∈ B (x = A ∧ φ) ↔ ∃!y ∈ B φ)
Theorem	reuxfr 1580	Transfer existential uniqueness from a variable x to another variable y contained in expression A.
⊢ (y ∈ B → A ∈ B)    &   ⊢ (x ∈ B → ∃!y ∈ B x = A)    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (∃!x ∈ B φ ↔ ∃!y ∈ B ψ)
Theorem	reuhyp 1581	A theorem useful for eliminating the restricted existential uniqueness hypotheses in reuxfr 1580.
⊢ (x ∈ C → B ∈ C)    &   ⊢ ((x ∈ C ∧ y ∈ C) → (x = A ↔ y = B))    ⇒   ⊢ (x ∈ C → ∃!y ∈ C x = A)
Theorem	difeq1 1582	Equality theorem for class difference.
⊢ (A = B → (A ∖ C) = (B ∖ C))
Theorem	difeq2 1583	Equality theorem for class difference.
⊢ (A = B → (C ∖ A) = (C ∖ B))
Theorem	difeq1i 1584	Inference adding difference to the right in a class equality.
⊢ A = B    ⇒   ⊢ (A ∖ C) = (B ∖ C)
Theorem	difeq2i 1585	Inference adding difference to the left in a class equality.
⊢ A = B    ⇒   ⊢ (C ∖ A) = (C ∖ B)
Theorem	difeq12i 1586	Equality inference for class difference.
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A ∖ C) = (B ∖ D)
Theorem	difeq1d 1587	Deduction adding difference to the right in a class equality.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ∖ C) = (B ∖ C))
Theorem	difeq2d 1588	Deduction adding difference to the left in a class equality.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ∖ A) = (C ∖ B))
Theorem	difeqri 1589	Inference from membership to difference.
⊢ ((x ∈ A ∧ ¬ x ∈ B) ↔ x ∈ C)    ⇒   ⊢ (A ∖ B) = C
Theorem	hbdif 1590	Bound-variable hypothesis builder for class difference.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (y ∈ (A ∖ B) → ∀x y ∈ (A ∖ B))
Theorem	eldifi 1591	Implication of membership in a class difference.
⊢ (A ∈ (B ∖ C) → A ∈ B)
Theorem	eldifn 1592	Implication of membership in a class difference.
⊢ (A ∈ (B ∖ C) → ¬ A ∈ C)
Theorem	elndif 1593	A set does not belong to a class excluding it.
⊢ (A ∈ B → ¬ A ∈ (C ∖ B))
Theorem	neldif 1594	Implication of membership in a class difference.
⊢ ((A ∈ B ∧ ¬ A ∈ (B ∖ C)) → A ∈ C)
Theorem	difdif 1595	Double class difference. Exercise 11 of [TakeutiZaring] p. 22.
⊢ (A ∖ (B ∖ A)) = A
Theorem	difss 1596	Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22.
⊢ (A ∖ B) ⊆ A
Theorem	ddif 1597	Double complement under universal class. Exercise 4.10(s) of [Mendelson] p. 231.
⊢ (V ∖ (V ∖ A)) = A
Theorem	ssconb 1598	Contraposition law for subsets.
⊢ ((A ⊆ C ∧ B ⊆ C) → (A ⊆ (C ∖ B) ↔ B ⊆ (C ∖ A)))
Theorem	sscon 1599	Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22.
⊢ (A ⊆ B → (C ∖ B) ⊆ (C ∖ A))
Theorem	ssdif 1600	Difference law for subsets.
⊢ (A ⊆ B → (A ∖ C) ⊆ (B ∖ C))