Metamath Proof Explorer - mmtheorems21

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 - 2001-2100 - Page 21 of 58

Type	Label	Description
Statement
Theorem	iuniin 2001	Law combining indexed union with indexed intersection.
⊢ ∪x ∈ A ∩y ∈ B C ⊆ ∩y ∈ B ∪x ∈ A C
Theorem	iunss1 2002	Subclass theorem for indexed union.
⊢ (A ⊆ B → ∪x ∈ A C ⊆ ∪x ∈ B C)
Theorem	iuneq1 2003	Equality theorem for indexed union.
⊢ (A = B → ∪x ∈ A C = ∪x ∈ B C)
Theorem	iineq1 2004	Equality theorem for restricted existential quantifier.
⊢ (A = B → ∩x ∈ A C = ∩x ∈ B C)
Theorem	ss2iun 2005	Subclass theorem for indexed union.
⊢ (∀x ∈ A B ⊆ C → ∪x ∈ A B ⊆ ∪x ∈ A C)
Theorem	iuneq2 2006	Equality theorem for indexed union.
⊢ (∀x ∈ A B = C → ∪x ∈ A B = ∪x ∈ A C)
Theorem	iineq2 2007	Equality theorem for indexed intersection.
⊢ (∀x ∈ A B = C → ∩x ∈ A B = ∩x ∈ A C)
Theorem	iuneq2i 2008	Equality inference for indexed union.
⊢ (x ∈ A → B = C)    ⇒   ⊢ ∪x ∈ A B = ∪x ∈ A C
Theorem	iineq2i 2009	Equality inference for indexed intersection.
⊢ (x ∈ A → B = C)    ⇒   ⊢ ∩x ∈ A B = ∩x ∈ A C
Theorem	iuneq2dv 2010	Equality deduction for indexed union.
⊢ (φ → (x ∈ A → B = C))    ⇒   ⊢ (φ → ∪x ∈ A B = ∪x ∈ A C)
Theorem	iineq2dv 2011	Equality deduction for indexed intersection.
⊢ (φ → (x ∈ A → B = C))    ⇒   ⊢ (φ → ∩x ∈ A B = ∩x ∈ A C)
Theorem	hbiu1 2012	Bound-variable hypothesis builder for indexed union.
⊢ (y ∈ ∪x ∈ A B → ∀x y ∈ ∪x ∈ A B)
Theorem	hbii1 2013	Bound-variable hypothesis builder for indexed intersection.
⊢ (y ∈ ∩x ∈ A B → ∀x y ∈ ∩x ∈ A B)
Theorem	dfiun2 2014	Alternate definition of indexed union when B is a set. Definition 15(a) of [Suppes] p. 44.
⊢ B ∈ V    ⇒   ⊢ ∪x ∈ A B = ∪{y∣∃x ∈ A y = B}
Theorem	dfiin2 2015	Alternate definition of indexed intersection when B is a set. Definition 15(b) of [Suppes] p. 44.
⊢ B ∈ V    ⇒   ⊢ ∩x ∈ A B = ∩{y∣∃x ∈ A y = B}
Theorem	cbviunv 2016	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis.
⊢ (x = y → B = C)    ⇒   ⊢ ∪x ∈ A B = ∪y ∈ A C
Theorem	iunss 2017	Subset theorem for an indexed union.
⊢ (∪x ∈ A B ⊆ C ↔ ∀x ∈ A B ⊆ C)
Theorem	ssiun 2018	Subset implication for an indexed union.
⊢ (∃x ∈ A C ⊆ B → C ⊆ ∪x ∈ A B)
Theorem	ssiun2 2019	Identity law for subset of an indexed union.
⊢ (x ∈ A → B ⊆ ∪x ∈ A B)
Theorem	ssiun2s 2020	Subset relationship for an indexed union.
⊢ (x = C → B = D)    ⇒   ⊢ (C ∈ A → D ⊆ ∪x ∈ A B)
Theorem	iunss2 2021	A subclass condition on the members of two indexed classes C(x) and D(y) that implies a subclass relation on their indexed unions. Generalization of Proposition 8.6 of [TakeutiZaring] p. 59. Compare uniss2 1942.
⊢ (∀x ∈ A ∃y ∈ B C ⊆ D → ∪x ∈ A C ⊆ ∪y ∈ B D)
Theorem	iunrab 2022	The indexed union of a restricted class abstraction.
⊢ ∪x ∈ A {y ∈ B∣φ} = {y ∈ B∣∃x ∈ A φ}
Theorem	iunab 2023	The indexed union of a class abstraction.
⊢ ∪x ∈ A {y∣φ} = {y∣∃x ∈ A φ}
Theorem	ssiin 2024	Subset theorem for an indexed intersection.
⊢ (C ⊆ ∩x ∈ A B ↔ ∀x ∈ A C ⊆ B)
Theorem	iinss 2025	Subset implication for an indexed intersection.
⊢ (∃x ∈ A B ⊆ C → ∩x ∈ A B ⊆ C)
Theorem	uniiun 2026	Class union in terms of indexed union. Definition of [Stoll] p. 43.
⊢ ∪A = ∪x ∈ A x
Theorem	intiin 2027	Class intersection in terms of indexed intersection. Definition of [Stoll] p. 44.
⊢ ∩A = ∩x ∈ A x
Theorem	iun0 2028	An indexed union of the empty set is empty.
⊢ ∪x ∈ A ∅ = ∅
Theorem	iunn0 2029	There is a non-empty class in an indexed collection B(x) iff the indexed union of them is non-empty.
⊢ (∃x ∈ A ¬ B = ∅ ↔ ¬ ∪x ∈ A B = ∅)
Theorem	iunin2 2030	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 2026 to recover Enderton's theorem.
⊢ ∪x ∈ A (B ∩ C) = (B ∩ ∪x ∈ A C)
Theorem	iinun2 2031	Indexed intersection of union. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 2027 to recover Enderton's theorem.
⊢ ∩x ∈ A (B ∪ C) = (B ∪ ∩x ∈ A C)
Theorem	iundif2 2032	Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use intiin 2027 to recover Enderton's theorem.
⊢ ∪x ∈ A (B ∖ C) = (B ∖ ∩x ∈ A C)
Theorem	iindif2 2033	Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use uniiun 2026 to recover Enderton's theorem.
⊢ (¬ A = ∅ → ∩x ∈ A (B ∖ C) = (B ∖ ∪x ∈ A C))
Theorem	iunxsn 2034	A singleton index picks out an instance of an indexed union's argument.
⊢ A ∈ V    &   ⊢ (x = A → B = C)    ⇒   ⊢ ∪x ∈ {A}B = C
Theorem	iunxun 2035	Separate a union in the index of an indexed union.
⊢ ∪x ∈ (A ∪ B)C = (∪x ∈ A C ∪ ∪x ∈ B C)
Theorem	iinuni 2036	A relationship involving union and indexed intersection. Exercise 23 of [Enderton] p. 33.
⊢ (A ∪ ∩B) = ∩x ∈ B (A ∪ x)
Theorem	iununi 2037	A relationship involving union and indexed union. Exercise 25 of [Enderton] p. 33.
⊢ ((B = ∅ → A = ∅) ↔ (A ∪ ∪B) = ∪x ∈ B (A ∪ x))
Theorem	iinpw 2038	The power class of an intersection in terms of indexed intersection. Exercise 24(a) of [Enderton] p. 33.
⊢ ℘∩A = ∩x ∈ A ℘x
Theorem	iunpwss 2039	Inclusion of an indexed intersection in the power class of a union. Part of Exercise 24(b) of [Enderton] p. 33.
⊢ ∪x ∈ A ℘x ⊆ ℘∪A
Theorem	iunpw 2040	The power class of an intersection in terms of indexed intersection. Part of Exercise 24(b) of [Enderton] p. 33.
⊢ A ∈ V    ⇒   ⊢ (∃x ∈ A x = ∪A ↔ ℘∪A = ∪x ∈ A ℘x)
Syntax	wtr 2041	Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35.
wff Tr A
Definition	df-tr 2042	Define a transitive class. Not to be confused with a transitive relation (see cotr 2625). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 2043 (which is suggestive of the word "transitive"), dftr3 2045, and dftr4 2046. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130.
⊢ (Tr A ↔ ∪A ⊆ A)
Theorem	dftr2 2043	An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40.
⊢ (Tr A ↔ ∀x∀y((x ∈ y ∧ y ∈ A) → x ∈ A))
Theorem	dftr5 2044	An alternate way of defining a transitive class.
⊢ (Tr A ↔ ∀x ∈ A ∀y ∈ x y ∈ A)
Theorem	dftr3 2045	An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35.
⊢ (Tr A ↔ ∀x ∈ A x ⊆ A)
Theorem	dftr4 2046	An alternate way of defining a transitive class. Definition of [Enderton] p. 71.
⊢ (Tr A ↔ A ⊆ ℘A)
Theorem	treq 2047	Equality theorem for the transitive class predicate.
⊢ (A = B → (Tr A ↔ Tr B))
Theorem	trel 2048	In a transitive class, the membership relation is transitive.
⊢ (Tr A → ((B ∈ C ∧ C ∈ A) → B ∈ A))
Theorem	trel3 2049	In a transitive class, the membership relation is transitive.
⊢ (Tr A → ((B ∈ C ∧ C ∈ D ∧ D ∈ A) → B ∈ A))
Theorem	trss 2050	An element of a transitive class is a subset of the class.
⊢ (Tr A → (B ∈ A → B ⊆ A))
Theorem	trin 2051	The intersection of transitive classes is transitive.
⊢ ((Tr A ∧ Tr B) → Tr (A ∩ B))
Theorem	tr0 2052	The empty set is transitive.
⊢ Tr ∅
Theorem	trv 2053	The universe is transitive.
⊢ Tr V
Syntax	wbr 2054	Extend wff notation to include the general binary relation predicate. Note that the syntax is simply three class symbols in a row.
wff ARB
Syntax	copab 2055	Extend class notation to include class abstractions of ordered pairs.
class {⟨x, y⟩∣φ}
Syntax	cep 2056	Extend class notation to include the epsilon relation.
class E
Syntax	cid 2057	Extend the definition of a class to include identity relation.
class I
Syntax	wpo 2058	Extend wff notation to include the partial ordering predicate. Read: 'R is a partial order on A.'
wff R Po A
Syntax	wor 2059	Extend wff notation to include the strict ordering predicate. Read: 'R orders A.'
wff R Or A
Syntax	csup 2060	Extend class notation to include supremum of class A. Here R is ordinarily a relation that strictly orders class B. For example, R could be 'less than' and B could be the set of real numbers.
class sup(A, B, R)
Syntax	wfr 2061	Extend wff notation to include the founded predicate. Read: 'R is a founded relation on A.'
wff R Fr A
Syntax	wwe 2062	Extend wff notation to include the well-ordering predicate. Read: 'R well-orders A.'
wff R We A
Definition	df-br 2063	Define a general binary relation. Note that the syntax is simply three class symbols in a row. Definition 6.18 of [TakeutiZaring] p. 29 generalized to arbitrary classes. Class R normally denotes a relation such as "<" that compares two classes A and B, which might be numbers such as 1 and 2. This definition is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets). On the other hand we often find uses for this definition when R is a proper class.
⊢ (ARB ↔ ⟨A, B⟩ ∈ R)
Theorem	breq 2064	Equality theorem for a binary relation.
⊢ (R = S → (ARB ↔ ASB))
Theorem	breq1 2065	Equality theorem for binary relation.
⊢ (A = B → (ARC ↔ BRC))
Theorem	breq2 2066	Equality theorem for binary relation.
⊢ (A = B → (CRA ↔ CRB))
Theorem	breq12 2067	Equality theorem for binary relation.
⊢ ((A = B ∧ C = D) → (ARC ↔ BRD))
Theorem	breq1i 2068	Equality inference for binary relation.
⊢ A = B    ⇒   ⊢ (ARC ↔ BRC)
Theorem	breq2i 2069	Equality inference for binary relation.
⊢ A = B    ⇒   ⊢ (CRA ↔ CRB)
Theorem	breq12i 2070	Equality inference for binary relation.
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (ARC ↔ BRD)
Theorem	breq1d 2071	Equality deduction for binary relation.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (ARC ↔ BRC))
Theorem	breq2d 2072	Equality deduction for binary relation.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (CRA ↔ CRB))
Theorem	breq12d 2073	Equality deduction for binary relation.
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (ARC ↔ BRD))
Theorem	breqan12d 2074	Equality deduction for binary relation.
⊢ (φ → A = B)    &   ⊢ (ψ → C = D)    ⇒   ⊢ ((φ ∧ ψ) → (ARC ↔ BRD))
Theorem	breqan12rd 2075	Equality deduction for binary relation.
⊢ (φ → A = B)    &   ⊢ (ψ → C = D)    ⇒   ⊢ ((ψ ∧ φ) → (ARC ↔ BRD))
Theorem	eqbrtr 2076	Substitution of equal classes into a binary relation.
⊢ A = B    &   ⊢ BRC    ⇒   ⊢ ARC
Theorem	eqbrtrd 2077	Substitution of equal classes into a binary relation.
⊢ (φ → A = B)    &   ⊢ (φ → BRC)    ⇒   ⊢ (φ → ARC)
Theorem	eqbrtrr 2078	Substitution of equal classes into a binary relation.
⊢ A = B    &   ⊢ ARC    ⇒   ⊢ BRC
Theorem	eqbrtrrd 2079	Substitution of equal classes into a binary relation.
⊢ (φ → A = B)    &   ⊢ (φ → ARC)    ⇒   ⊢ (φ → BRC)
Theorem	breqtr 2080	Substitution of equal classes into a binary relation.
⊢ ARB    &   ⊢ B = C    ⇒   ⊢ ARC
Theorem	breqtrd 2081	Substitution of equal classes into a binary relation.
⊢ (φ → ARB)    &   ⊢ (φ → B = C)    ⇒   ⊢ (φ → ARC)
Theorem	breqtrr 2082	Substitution of equal classes into a binary relation.
⊢ ARB    &   ⊢ C = B    ⇒   ⊢ ARC
Theorem	breqtrrd 2083	Substitution of equal classes into a binary relation.
⊢ (φ → ARB)    &   ⊢ (φ → C = B)    ⇒   ⊢ (φ → ARC)
Theorem	3brtr3 2084	Substitution of equality into both sides of a binary relation.
⊢ ARB    &   ⊢ A = C    &   ⊢ B = D    ⇒   ⊢ CRD
Theorem	3brtr4 2085	Substitution of equality into both sides of a binary relation.
⊢ ARB    &   ⊢ C = A    &   ⊢ D = B    ⇒   ⊢ CRD
Theorem	3brtr3d 2086	Substitution of equality into both sides of a binary relation.
⊢ (φ → ARB)    &   ⊢ (φ → A = C)    &   ⊢ (φ → B = D)    ⇒   ⊢ (φ → CRD)
Theorem	3brtr3g 2087	Substitution of equality into both sides of a binary relation.
⊢ (φ → ARB)    &   ⊢ A = C    &   ⊢ B = D    ⇒   ⊢ (φ → CRD)
Theorem	3brtr4g 2088	Substitution of equality into both sides of a binary relation.
⊢ (φ → ARB)    &   ⊢ C = A    &   ⊢ D = B    ⇒   ⊢ (φ → CRD)
Theorem	syl5eqbr 2089	A chained equality inference for a binary relation.
⊢ (φ → ARB)    &   ⊢ C = A    ⇒   ⊢ (φ → CRB)
Theorem	syl5eqbrr 2090	A chained equality inference for a binary relation.
⊢ (φ → ARB)    &   ⊢ A = C    ⇒   ⊢ (φ → CRB)
Theorem	syl5breq 2091	A chained equality inference for a binary relation.
⊢ (φ → A = B)    &   ⊢ CRA    ⇒   ⊢ (φ → CRB)
Theorem	syl6eqbr 2092	A chained equality inference for a binary relation.
⊢ (φ → A = B)    &   ⊢ BRC    ⇒   ⊢ (φ → ARC)
Theorem	syl6breq 2093	A chained equality inference for a binary relation.
⊢ (φ → ARB)    &   ⊢ B = C    ⇒   ⊢ (φ → ARC)
Theorem	ssbrd 2094	Deduction from a subclass relationship of binary relations.
⊢ (φ → A ⊆ B)    ⇒   ⊢ (φ → (CAD → CBD))
Theorem	hbbr 2095	Bound-variable hypothesis builder for binary relation.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ R → ∀x y ∈ R)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (ARB → ∀x ARB)
Theorem	brab1 2096	Relationship between a binary relation and a class abstraction.
⊢ (xRy ↔ x ∈ {z∣zRy})
Theorem	brprc 2097	A property of proper class as the second argument of a binary relation.
⊢ (¬ B ∈ V → (ARB ↔ ARA))
Definition	df-opab 2098	Define class abstractions of ordered pairs. Definition 3.3 of [Monk1] p. 34. Normally x and y are distinct, although the definition doesn't strictly require it.
⊢ {⟨x, y⟩∣φ} = {z∣∃x∃y(z = ⟨x, y⟩ ∧ φ)}
Theorem	opabid 2099	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
⊢ (⟨x, y⟩ ∈ {⟨x, y⟩∣φ} ↔ φ)
Theorem	opabss 2100	The collection of ordered pairs in a class is a subclass of it.
⊢ {⟨x, y⟩∣xRy} ⊆ R