Metamath Proof Explorer - mmtheorems17

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 - 1601-1700 - Page 17 of 58

Type	Label	Description
Statement
Theorem	elun 1601	Expansion of membership in class union. Theorem 12 of [Suppes] p. 25.
⊢ (A ∈ (B ∪ C) ↔ (A ∈ B ∨ A ∈ C))
Theorem	uneqri 1602	Inference from membership to union.
⊢ ((x ∈ A ∨ x ∈ B) ↔ x ∈ C)    ⇒   ⊢ (A ∪ B) = C
Theorem	unidm 1603	Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27.
⊢ (A ∪ A) = A
Theorem	uncom 1604	Commutative law for union of classes. Exercise 6 of [TakeutiZaring] p. 17.
⊢ (A ∪ B) = (B ∪ A)
Theorem	uneq1 1605	Equality theorem for union of two classes.
⊢ (A = B → (A ∪ C) = (B ∪ C))
Theorem	uneq2 1606	Equality theorem for the union of two classes.
⊢ (A = B → (C ∪ A) = (C ∪ B))
Theorem	uneq1i 1607	Inference adding union to the right in a class equality.
⊢ A = B    ⇒   ⊢ (A ∪ C) = (B ∪ C)
Theorem	uneq2i 1608	Inference adding union to the left in a class equality.
⊢ A = B    ⇒   ⊢ (C ∪ A) = (C ∪ B)
Theorem	uneq12i 1609	Equality inference for union of two classes.
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A ∪ C) = (B ∪ D)
Theorem	uneq1d 1610	Deduction adding union to the right in a class equality.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ∪ C) = (B ∪ C))
Theorem	uneq2d 1611	Deduction adding union to the left in a class equality.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ∪ A) = (C ∪ B))
Theorem	uneq12d 1612	Equality deduction for intersection of two classes.
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A ∪ C) = (B ∪ D))
Theorem	uneq12 1613	Equality theorem for union of two classes.
⊢ ((A = B ∧ C = D) → (A ∪ C) = (B ∪ D))
Theorem	hbun 1614	Bound-variable hypothesis builder for the union of classes.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (y ∈ (A ∪ B) → ∀x y ∈ (A ∪ B))
Theorem	unass 1615	Associative law for union of classes. Exercise 8 of [TakeutiZaring] p. 17.
⊢ ((A ∪ B) ∪ C) = (A ∪ (B ∪ C))
Theorem	un12 1616	A rearrangement of union.
⊢ (A ∪ (B ∪ C)) = (B ∪ (A ∪ C))
Theorem	un23 1617	A rearrangement of union.
⊢ ((A ∪ B) ∪ C) = ((A ∪ C) ∪ B)
Theorem	un4 1618	A rearrangement of the union of 4 classes.
⊢ ((A ∪ B) ∪ (C ∪ D)) = ((A ∪ C) ∪ (B ∪ D))
Theorem	unundi 1619	Union distributes over itself.
⊢ (A ∪ (B ∪ C)) = ((A ∪ B) ∪ (A ∪ C))
Theorem	unundir 1620	Union distributes over itself.
⊢ ((A ∪ B) ∪ C) = ((A ∪ C) ∪ (B ∪ C))
Theorem	ssun1 1621	Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27.
⊢ A ⊆ (A ∪ B)
Theorem	ssun2 1622	Subclass relationship for union of classes.
⊢ A ⊆ (B ∪ A)
Theorem	ssun3 1623	Subclass law for union of classes.
⊢ (A ⊆ B → A ⊆ (B ∪ C))
Theorem	ssun4 1624	Subclass law for union of classes.
⊢ (A ⊆ B → A ⊆ (C ∪ B))
Theorem	elun1 1625	Membership law for union of classes.
⊢ (A ∈ B → A ∈ (B ∪ C))
Theorem	elun2 1626	Membership law for union of classes.
⊢ (A ∈ B → A ∈ (C ∪ B))
Theorem	unss1 1627	Subclass law for union of classes.
⊢ (A ⊆ B → (A ∪ C) ⊆ (B ∪ C))
Theorem	ssequn1 1628	A relationship between subclass and union. Theorem 26 of [Suppes] p. 27.
⊢ (A ⊆ B ↔ (A ∪ B) = B)
Theorem	unss2 1629	Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18.
⊢ (A ⊆ B → (C ∪ A) ⊆ (C ∪ B))
Theorem	unss12 1630	Subclass law for union of classes.
⊢ ((A ⊆ B ∧ C ⊆ D) → (A ∪ C) ⊆ (B ∪ D))
Theorem	ssequn2 1631	A relationship between subclass and union.
⊢ (A ⊆ B ↔ (B ∪ A) = B)
Theorem	unss 1632	The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse.
⊢ ((A ⊆ C ∧ B ⊆ C) ↔ (A ∪ B) ⊆ C)
Theorem	unssi 1633	An inference that the union of two subclasses is a subclass. Contributed by Raph Levien, 10-Dec-02.
⊢ A ⊆ C    &   ⊢ B ⊆ C    ⇒   ⊢ (A ∪ B) ⊆ C
Theorem	ssun 1634	A condition that implies inclusion in the union of two classes.
⊢ ((A ⊆ B ∨ A ⊆ C) → A ⊆ (B ∪ C))
Theorem	elin 1635	Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25.
⊢ (A ∈ (B ∩ C) ↔ (A ∈ B ∧ A ∈ C))
Theorem	incom 1636	Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17.
⊢ (A ∩ B) = (B ∩ A)
Theorem	ineqri 1637	Inference from membership to intersection.
⊢ ((x ∈ A ∧ x ∈ B) ↔ x ∈ C)    ⇒   ⊢ (A ∩ B) = C
Theorem	ineq1 1638	Equality theorem for intersection of two classes.
⊢ (A = B → (A ∩ C) = (B ∩ C))
Theorem	ineq2 1639	Equality theorem for intersection of two classes.
⊢ (A = B → (C ∩ A) = (C ∩ B))
Theorem	ineq12 1640	Equality theorem for intersection of two classes.
⊢ ((A = B ∧ C = D) → (A ∩ C) = (B ∩ D))
Theorem	ineq1i 1641	Equality inference for intersection of two classes.
⊢ A = B    ⇒   ⊢ (A ∩ C) = (B ∩ C)
Theorem	ineq2i 1642	Equality inference for intersection of two classes.
⊢ A = B    ⇒   ⊢ (C ∩ A) = (C ∩ B)
Theorem	ineq12i 1643	Equality inference for intersection of two classes.
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A ∩ C) = (B ∩ D)
Theorem	ineq1d 1644	Equality deduction for intersection of two classes.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ∩ C) = (B ∩ C))
Theorem	ineq2d 1645	Equality deduction for intersection of two classes.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ∩ A) = (C ∩ B))
Theorem	ineq12d 1646	Equality deduction for intersection of two classes.
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A ∩ C) = (B ∩ D))
Theorem	hbin 1647	Bound-variable hypothesis builder for the intersection of classes.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (y ∈ (A ∩ B) → ∀x y ∈ (A ∩ B))
Theorem	birabrdv 1648	Deduction from wff to restricted class abstraction.
⊢ (φ → (x ∈ B → (x ∈ A ↔ χ)))    ⇒   ⊢ (φ → (B ∩ A) = {x ∈ B∣χ})
Theorem	inidm 1649	Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26.
⊢ (A ∩ A) = A
Theorem	inass 1650	Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17.
⊢ ((A ∩ B) ∩ C) = (A ∩ (B ∩ C))
Theorem	in12 1651	A rearrangement of intersection.
⊢ (A ∩ (B ∩ C)) = (B ∩ (A ∩ C))
Theorem	in23 1652	A rearrangement of intersection.
⊢ ((A ∩ B) ∩ C) = ((A ∩ C) ∩ B)
Theorem	in4 1653	Rearrangement of intersection of 4 classes.
⊢ ((A ∩ B) ∩ (C ∩ D)) = ((A ∩ C) ∩ (B ∩ D))
Theorem	inindi 1654	Intersection distributes over itself.
⊢ (A ∩ (B ∩ C)) = ((A ∩ B) ∩ (A ∩ C))
Theorem	inindir 1655	Intersection distributes over itself.
⊢ ((A ∩ B) ∩ C) = ((A ∩ C) ∩ (B ∩ C))
Theorem	sseqin2 1656	A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18.
⊢ (A ⊆ B ↔ (B ∩ A) = A)
Theorem	inss1 1657	The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18.
⊢ (A ∩ B) ⊆ A
Theorem	inss2 1658	The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18.
⊢ (A ∩ B) ⊆ B
Theorem	ssin 1659	Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26.
⊢ ((A ⊆ B ∧ A ⊆ C) ↔ A ⊆ (B ∩ C))
Theorem	ssini 1660	An inference showing that the a subclass of two classes is a subclass of their intersection.
⊢ A ⊆ B    &   ⊢ A ⊆ C    ⇒   ⊢ A ⊆ (B ∩ C)
Theorem	ssrin 1661	Add right intersection to subclass relation.
⊢ (A ⊆ B → (A ∩ C) ⊆ (B ∩ C))
Theorem	sslin 1662	Add left intersection to subclass relation.
⊢ (A ⊆ B → (C ∩ A) ⊆ (C ∩ B))
Theorem	ss2in 1663	Intersection of subclasses.
⊢ ((A ⊆ B ∧ C ⊆ D) → (A ∩ C) ⊆ (B ∩ D))
Theorem	ssinss1 1664	Intersection preserves subclass relationship.
⊢ (A ⊆ C → (A ∩ B) ⊆ C)
Theorem	nssinpss 1665	Negation of subclass expressed in terms of intersection and proper subclass.
⊢ (¬ A ⊆ B ↔ (A ∩ B) ⊂ A)
Theorem	nsspssun 1666	Negation of subclass expressed in terms of proper subclass and union.
⊢ (¬ A ⊆ B ↔ B ⊂ (A ∪ B))
Theorem	dfss4 1667	Subclass defined in terms of class difference. See comments under dfun2 1668.
⊢ (A ⊆ B ↔ (B ∖ (B ∖ A)) = A)
Theorem	dfun2 1668	An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 1669 and dfss4 1667 it shows we can express union, intersection, and subset directly in terms of the single "primitive" operation ∖ (class difference).
⊢ (A ∪ B) = (V ∖ ((V ∖ A) ∖ B))
Theorem	dfin2 1669	An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 1668. Another version is given by dfin4 1673.
⊢ (A ∩ B) = (A ∖ (V ∖ B))
Theorem	difin 1670	Difference with intersection. Theorem 33 of [Suppes] p. 29.
⊢ (A ∖ (A ∩ B)) = (A ∖ B)
Theorem	dfun3 1671	Union defined in terms of intersection (DeMorgan's law). Definition of union in [Mendelson] p. 231.
⊢ (A ∪ B) = (V ∖ ((V ∖ A) ∩ (V ∖ B)))
Theorem	dfin3 1672	Intersection defined in terms of union (DeMorgan's law. Similar to Exercise 4.10(n) of [Mendelson] p. 231.
⊢ (A ∩ B) = (V ∖ ((V ∖ A) ∪ (V ∖ B)))
Theorem	dfin4 1673	Alternate definition of the union of two classes. Exercise 4.10(q) of [Mendelson] p. 231.
⊢ (A ∩ B) = (A ∖ (A ∖ B))
Theorem	invdif 1674	Intersection with universal complement. Remark in [Stoll] p. 20.
⊢ (A ∩ (V ∖ B)) = (A ∖ B)
Theorem	indif 1675	Intersection with class difference. Theorem 34 of [Suppes] p. 29.
⊢ (A ∩ (A ∖ B)) = (A ∖ B)
Theorem	indi 1676	Distributive law for intersection over union. Exercise 10 of [TakeutiZaring] p. 17.
⊢ (A ∩ (B ∪ C)) = ((A ∩ B) ∪ (A ∩ C))
Theorem	undi 1677	Distributive law for union over intersection. Exercise 11 of [TakeutiZaring] p. 17.
⊢ (A ∪ (B ∩ C)) = ((A ∪ B) ∩ (A ∪ C))
Theorem	indir 1678	Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27.
⊢ ((A ∪ B) ∩ C) = ((A ∩ C) ∪ (B ∩ C))
Theorem	undir 1679	Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27.
⊢ ((A ∩ B) ∪ C) = ((A ∪ C) ∩ (B ∪ C))
Theorem	unineq 1680	Deduce equality from equalities of union and intersection. Exercise 20 of [Enderton] p. 32 and its converse.
⊢ (((A ∪ C) = (B ∪ C) ∧ (A ∩ C) = (B ∩ C)) ↔ A = B)
Theorem	difundi 1681	Distributive law for class difference. Theorem 39 of [Suppes] p. 29.
⊢ (A ∖ (B ∪ C)) = ((A ∖ B) ∩ (A ∖ C))
Theorem	difundir 1682	Distributive law for class difference.
⊢ ((A ∪ B) ∖ C) = ((A ∖ C) ∪ (B ∖ C))
Theorem	difindi 1683	Distributive law for class difference. Theorem 40 of [Suppes] p. 29.
⊢ (A ∖ (B ∩ C)) = ((A ∖ B) ∪ (A ∖ C))
Theorem	difindir 1684	Distributive law for class difference.
⊢ ((A ∩ B) ∖ C) = ((A ∖ C) ∩ (B ∖ C))
Theorem	undm 1685	DeMorgan's law for union. Theorem 5.2(13) of [Stoll] p. 19.
⊢ (V ∖ (A ∪ B)) = ((V ∖ A) ∩ (V ∖ B))
Theorem	indm 1686	DeMorgan's law for intersection. Theorem 5.2(13') of [Stoll] p. 19.
⊢ (V ∖ (A ∩ B)) = ((V ∖ A) ∪ (V ∖ B))
Theorem	difun1 1687	A relationship involving double difference and union.
⊢ (A ∖ (B ∪ C)) = ((A ∖ B) ∖ C)
Theorem	dif23 1688	Swap second and third argument of double difference.
⊢ ((A ∖ B) ∖ C) = ((A ∖ C) ∖ B)
Theorem	symdif1 1689	Two ways of expressing symmetric difference. This theorem shows the equivalence of the definition of symmetric difference in [Stoll] p. 13 and the restated definition in Example 4.1 of [Stoll] p. 262.
⊢ ((A ∖ B) ∪ (B ∖ A)) = ((A ∪ B) ∖ (A ∩ B))
Theorem	symdif2 1690	Two ways of expressing symmetric difference.
⊢ ((A ∖ B) ∪ (B ∖ A)) = {x∣ ¬ (x ∈ A ↔ x ∈ B)}
Theorem	unab 1691	Union of two class abstractions.
⊢ ({x∣φ} ∪ {x∣ψ}) = {x∣(φ ∨ ψ)}
Theorem	inab 1692	Intersection of two class abstractions.
⊢ ({x∣φ} ∩ {x∣ψ}) = {x∣(φ ∧ ψ)}
Theorem	difab 1693	Difference of two class abstractions.
⊢ ({x∣φ} ∖ {x∣ψ}) = {x∣(φ ∧ ¬ ψ)}
Theorem	unrab 1694	Union of two restricted class abstractions.
⊢ ({x ∈ A∣φ} ∪ {x ∈ A∣ψ}) = {x ∈ A∣(φ ∨ ψ)}
Theorem	difrab 1695	Difference of two restricted class abstractions.
⊢ ({x ∈ A∣φ} ∖ {x ∈ A∣ψ}) = {x ∈ A∣(φ ∧ ¬ ψ)}
Theorem	dfrab2 1696	Alternate definition of restricted class abstraction.
⊢ {x ∈ A∣φ} = ({x∣φ} ∩ A)
Theorem	inex1 1697	Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22.
⊢ A ∈ V    ⇒   ⊢ (A ∩ B) ∈ V
Theorem	inex2 1698	Separation Scheme (Aussonderung) using class notation.
⊢ A ∈ V    ⇒   ⊢ (B ∩ A) ∈ V
Theorem	inex1g 1699	Closed-form, generalized Separation Scheme.
⊢ (A ∈ C → (A ∩ B) ∈ V)
Theorem	ssex 1700	The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way of expressing the Axiom of Separation zfaus 1480 (a.k.a. Subset Axiom).
⊢ B ∈ V    ⇒   ⊢ (A ⊆ B → A ∈ V)