Theorem List for Intuitionistic Logic Explorer - 4901-5000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | cnvdif 4901 |
Distributive law for converse over set difference. (Contributed by
Mario Carneiro, 26-Jun-2014.)
|
⊢ ◡(𝐴 ∖ 𝐵) = (◡𝐴 ∖ ◡𝐵) |
|
Theorem | cnvin 4902 |
Distributive law for converse over intersection. Theorem 15 of [Suppes]
p. 62. (Contributed by NM, 25-Mar-1998.) (Revised by Mario Carneiro,
26-Jun-2014.)
|
⊢ ◡(𝐴 ∩ 𝐵) = (◡𝐴 ∩ ◡𝐵) |
|
Theorem | rnun 4903 |
Distributive law for range over union. Theorem 8 of [Suppes] p. 60.
(Contributed by NM, 24-Mar-1998.)
|
⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵) |
|
Theorem | rnin 4904 |
The range of an intersection belongs the intersection of ranges. Theorem
9 of [Suppes] p. 60. (Contributed by NM,
15-Sep-2004.)
|
⊢ ran (𝐴 ∩ 𝐵) ⊆ (ran 𝐴 ∩ ran 𝐵) |
|
Theorem | rniun 4905 |
The range of an indexed union. (Contributed by Mario Carneiro,
29-May-2015.)
|
⊢ ran ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 ran 𝐵 |
|
Theorem | rnuni 4906* |
The range of a union. Part of Exercise 8 of [Enderton] p. 41.
(Contributed by NM, 17-Mar-2004.) (Revised by Mario Carneiro,
29-May-2015.)
|
⊢ ran ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ran 𝑥 |
|
Theorem | imaundi 4907 |
Distributive law for image over union. Theorem 35 of [Suppes] p. 65.
(Contributed by NM, 30-Sep-2002.)
|
⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) |
|
Theorem | imaundir 4908 |
The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
|
⊢ ((𝐴 ∪ 𝐵) “ 𝐶) = ((𝐴 “ 𝐶) ∪ (𝐵 “ 𝐶)) |
|
Theorem | dminss 4909 |
An upper bound for intersection with a domain. Theorem 40 of [Suppes]
p. 66, who calls it "somewhat surprising." (Contributed by
NM,
11-Aug-2004.)
|
⊢ (dom 𝑅 ∩ 𝐴) ⊆ (◡𝑅 “ (𝑅 “ 𝐴)) |
|
Theorem | imainss 4910 |
An upper bound for intersection with an image. Theorem 41 of [Suppes]
p. 66. (Contributed by NM, 11-Aug-2004.)
|
⊢ ((𝑅 “ 𝐴) ∩ 𝐵) ⊆ (𝑅 “ (𝐴 ∩ (◡𝑅 “ 𝐵))) |
|
Theorem | inimass 4911 |
The image of an intersection (Contributed by Thierry Arnoux,
16-Dec-2017.)
|
⊢ ((𝐴 ∩ 𝐵) “ 𝐶) ⊆ ((𝐴 “ 𝐶) ∩ (𝐵 “ 𝐶)) |
|
Theorem | inimasn 4912 |
The intersection of the image of singleton (Contributed by Thierry
Arnoux, 16-Dec-2017.)
|
⊢ (𝐶 ∈ 𝑉 → ((𝐴 ∩ 𝐵) “ {𝐶}) = ((𝐴 “ {𝐶}) ∩ (𝐵 “ {𝐶}))) |
|
Theorem | cnvxp 4913 |
The converse of a cross product. Exercise 11 of [Suppes] p. 67.
(Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴) |
|
Theorem | xp0 4914 |
The cross product with the empty set is empty. Part of Theorem 3.13(ii)
of [Monk1] p. 37. (Contributed by NM,
12-Apr-2004.)
|
⊢ (𝐴 × ∅) =
∅ |
|
Theorem | xpmlem 4915* |
The cross product of inhabited classes is inhabited. (Contributed by
Jim Kingdon, 11-Dec-2018.)
|
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) ↔ ∃𝑧 𝑧 ∈ (𝐴 × 𝐵)) |
|
Theorem | xpm 4916* |
The cross product of inhabited classes is inhabited. (Contributed by
Jim Kingdon, 13-Dec-2018.)
|
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) ↔ ∃𝑧 𝑧 ∈ (𝐴 × 𝐵)) |
|
Theorem | xpeq0r 4917 |
A cross product is empty if at least one member is empty. (Contributed by
Jim Kingdon, 12-Dec-2018.)
|
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅) |
|
Theorem | sqxpeq0 4918 |
A Cartesian square is empty iff its member is empty. (Contributed by Jim
Kingdon, 21-Apr-2023.)
|
⊢ ((𝐴 × 𝐴) = ∅ ↔ 𝐴 = ∅) |
|
Theorem | xpdisj1 4919 |
Cross products with disjoint sets are disjoint. (Contributed by NM,
13-Sep-2004.)
|
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 × 𝐶) ∩ (𝐵 × 𝐷)) = ∅) |
|
Theorem | xpdisj2 4920 |
Cross products with disjoint sets are disjoint. (Contributed by NM,
13-Sep-2004.)
|
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 × 𝐴) ∩ (𝐷 × 𝐵)) = ∅) |
|
Theorem | xpsndisj 4921 |
Cross products with two different singletons are disjoint. (Contributed
by NM, 28-Jul-2004.)
|
⊢ (𝐵 ≠ 𝐷 → ((𝐴 × {𝐵}) ∩ (𝐶 × {𝐷})) = ∅) |
|
Theorem | djudisj 4922* |
Disjoint unions with disjoint index sets are disjoint. (Contributed by
Stefan O'Rear, 21-Nov-2014.)
|
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐶) ∩ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝐷)) = ∅) |
|
Theorem | resdisj 4923 |
A double restriction to disjoint classes is the empty set. (Contributed
by NM, 7-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 ↾ 𝐴) ↾ 𝐵) = ∅) |
|
Theorem | rnxpm 4924* |
The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37,
with nonempty changed to inhabited. (Contributed by Jim Kingdon,
12-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ran (𝐴 × 𝐵) = 𝐵) |
|
Theorem | dmxpss 4925 |
The domain of a cross product is a subclass of the first factor.
(Contributed by NM, 19-Mar-2007.)
|
⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 |
|
Theorem | rnxpss 4926 |
The range of a cross product is a subclass of the second factor.
(Contributed by NM, 16-Jan-2006.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
⊢ ran (𝐴 × 𝐵) ⊆ 𝐵 |
|
Theorem | dmxpss2 4927 |
Upper bound for the domain of a binary relation. (Contributed by BJ,
10-Jul-2022.)
|
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → dom 𝑅 ⊆ 𝐴) |
|
Theorem | rnxpss2 4928 |
Upper bound for the range of a binary relation. (Contributed by BJ,
10-Jul-2022.)
|
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → ran 𝑅 ⊆ 𝐵) |
|
Theorem | rnxpid 4929 |
The range of a square cross product. (Contributed by FL,
17-May-2010.)
|
⊢ ran (𝐴 × 𝐴) = 𝐴 |
|
Theorem | ssxpbm 4930* |
A cross-product subclass relationship is equivalent to the relationship
for its components. (Contributed by Jim Kingdon, 12-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ (𝐴 × 𝐵) → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷))) |
|
Theorem | ssxp1 4931* |
Cross product subset cancellation. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) ⊆ (𝐵 × 𝐶) ↔ 𝐴 ⊆ 𝐵)) |
|
Theorem | ssxp2 4932* |
Cross product subset cancellation. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) ⊆ (𝐶 × 𝐵) ↔ 𝐴 ⊆ 𝐵)) |
|
Theorem | xp11m 4933* |
The cross product of inhabited classes is one-to-one. (Contributed by
Jim Kingdon, 13-Dec-2018.)
|
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
|
Theorem | xpcanm 4934* |
Cancellation law for cross-product. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) = (𝐶 × 𝐵) ↔ 𝐴 = 𝐵)) |
|
Theorem | xpcan2m 4935* |
Cancellation law for cross-product. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) = (𝐵 × 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | xpexr2m 4936* |
If a nonempty cross product is a set, so are both of its components.
(Contributed by Jim Kingdon, 14-Dec-2018.)
|
⊢ (((𝐴 × 𝐵) ∈ 𝐶 ∧ ∃𝑥 𝑥 ∈ (𝐴 × 𝐵)) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
|
Theorem | ssrnres 4937 |
Subset of the range of a restriction. (Contributed by NM,
16-Jan-2006.)
|
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵) |
|
Theorem | rninxp 4938* |
Range of the intersection with a cross product. (Contributed by NM,
17-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ (ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐶𝑦) |
|
Theorem | dminxp 4939* |
Domain of the intersection with a cross product. (Contributed by NM,
17-Jan-2006.)
|
⊢ (dom (𝐶 ∩ (𝐴 × 𝐵)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥𝐶𝑦) |
|
Theorem | imainrect 4940 |
Image of a relation restricted to a rectangular region. (Contributed by
Stefan O'Rear, 19-Feb-2015.)
|
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) “ 𝑌) = ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵) |
|
Theorem | xpima1 4941 |
The image by a cross product. (Contributed by Thierry Arnoux,
16-Dec-2017.)
|
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅) |
|
Theorem | xpima2m 4942* |
The image by a cross product. (Contributed by Thierry Arnoux,
16-Dec-2017.)
|
⊢ (∃𝑥 𝑥 ∈ (𝐴 ∩ 𝐶) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵) |
|
Theorem | xpimasn 4943 |
The image of a singleton by a cross product. (Contributed by Thierry
Arnoux, 14-Jan-2018.)
|
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) |
|
Theorem | cnvcnv3 4944* |
The set of all ordered pairs in a class is the same as the double
converse. (Contributed by Mario Carneiro, 16-Aug-2015.)
|
⊢ ◡◡𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} |
|
Theorem | dfrel2 4945 |
Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25.
(Contributed by NM, 29-Dec-1996.)
|
⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅) |
|
Theorem | dfrel4v 4946* |
A relation can be expressed as the set of ordered pairs in it.
(Contributed by Mario Carneiro, 16-Aug-2015.)
|
⊢ (Rel 𝑅 ↔ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦}) |
|
Theorem | cnvcnv 4947 |
The double converse of a class strips out all elements that are not
ordered pairs. (Contributed by NM, 8-Dec-2003.)
|
⊢ ◡◡𝐴 = (𝐴 ∩ (V × V)) |
|
Theorem | cnvcnv2 4948 |
The double converse of a class equals its restriction to the universe.
(Contributed by NM, 8-Oct-2007.)
|
⊢ ◡◡𝐴 = (𝐴 ↾ V) |
|
Theorem | cnvcnvss 4949 |
The double converse of a class is a subclass. Exercise 2 of
[TakeutiZaring] p. 25. (Contributed
by NM, 23-Jul-2004.)
|
⊢ ◡◡𝐴 ⊆ 𝐴 |
|
Theorem | cnveqb 4950 |
Equality theorem for converse. (Contributed by FL, 19-Sep-2011.)
|
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ◡𝐴 = ◡𝐵)) |
|
Theorem | cnveq0 4951 |
A relation empty iff its converse is empty. (Contributed by FL,
19-Sep-2011.)
|
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ◡𝐴 = ∅)) |
|
Theorem | dfrel3 4952 |
Alternate definition of relation. (Contributed by NM, 14-May-2008.)
|
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅) |
|
Theorem | dmresv 4953 |
The domain of a universal restriction. (Contributed by NM,
14-May-2008.)
|
⊢ dom (𝐴 ↾ V) = dom 𝐴 |
|
Theorem | rnresv 4954 |
The range of a universal restriction. (Contributed by NM,
14-May-2008.)
|
⊢ ran (𝐴 ↾ V) = ran 𝐴 |
|
Theorem | dfrn4 4955 |
Range defined in terms of image. (Contributed by NM, 14-May-2008.)
|
⊢ ran 𝐴 = (𝐴 “ V) |
|
Theorem | csbrng 4956 |
Distribute proper substitution through the range of a class.
(Contributed by Alan Sare, 10-Nov-2012.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵) |
|
Theorem | rescnvcnv 4957 |
The restriction of the double converse of a class. (Contributed by NM,
8-Apr-2007.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ (◡◡𝐴 ↾ 𝐵) = (𝐴 ↾ 𝐵) |
|
Theorem | cnvcnvres 4958 |
The double converse of the restriction of a class. (Contributed by NM,
3-Jun-2007.)
|
⊢ ◡◡(𝐴 ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵) |
|
Theorem | imacnvcnv 4959 |
The image of the double converse of a class. (Contributed by NM,
8-Apr-2007.)
|
⊢ (◡◡𝐴 “ 𝐵) = (𝐴 “ 𝐵) |
|
Theorem | dmsnm 4960* |
The domain of a singleton is inhabited iff the singleton argument is an
ordered pair. (Contributed by Jim Kingdon, 15-Dec-2018.)
|
⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥 𝑥 ∈ dom {𝐴}) |
|
Theorem | rnsnm 4961* |
The range of a singleton is inhabited iff the singleton argument is an
ordered pair. (Contributed by Jim Kingdon, 15-Dec-2018.)
|
⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥 𝑥 ∈ ran {𝐴}) |
|
Theorem | dmsn0 4962 |
The domain of the singleton of the empty set is empty. (Contributed by
NM, 30-Jan-2004.)
|
⊢ dom {∅} = ∅ |
|
Theorem | cnvsn0 4963 |
The converse of the singleton of the empty set is empty. (Contributed by
Mario Carneiro, 30-Aug-2015.)
|
⊢ ◡{∅} = ∅ |
|
Theorem | dmsn0el 4964 |
The domain of a singleton is empty if the singleton's argument contains
the empty set. (Contributed by NM, 15-Dec-2008.)
|
⊢ (∅ ∈ 𝐴 → dom {𝐴} = ∅) |
|
Theorem | relsn2m 4965* |
A singleton is a relation iff it has an inhabited domain. (Contributed
by Jim Kingdon, 16-Dec-2018.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (Rel {𝐴} ↔ ∃𝑥 𝑥 ∈ dom {𝐴}) |
|
Theorem | dmsnopg 4966 |
The domain of a singleton of an ordered pair is the singleton of the
first member. (Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐵 ∈ 𝑉 → dom {〈𝐴, 𝐵〉} = {𝐴}) |
|
Theorem | dmpropg 4967 |
The domain of an unordered pair of ordered pairs. (Contributed by Mario
Carneiro, 26-Apr-2015.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶}) |
|
Theorem | dmsnop 4968 |
The domain of a singleton of an ordered pair is the singleton of the
first member. (Contributed by NM, 30-Jan-2004.) (Proof shortened by
Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ dom {〈𝐴, 𝐵〉} = {𝐴} |
|
Theorem | dmprop 4969 |
The domain of an unordered pair of ordered pairs. (Contributed by NM,
13-Sep-2011.)
|
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶} |
|
Theorem | dmtpop 4970 |
The domain of an unordered triple of ordered pairs. (Contributed by NM,
14-Sep-2011.)
|
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐹 ∈
V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉} = {𝐴, 𝐶, 𝐸} |
|
Theorem | cnvcnvsn 4971 |
Double converse of a singleton of an ordered pair. (Unlike cnvsn 4977,
this does not need any sethood assumptions on 𝐴 and 𝐵.)
(Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ ◡◡{〈𝐴, 𝐵〉} = ◡{〈𝐵, 𝐴〉} |
|
Theorem | dmsnsnsng 4972 |
The domain of the singleton of the singleton of a singleton.
(Contributed by Jim Kingdon, 16-Dec-2018.)
|
⊢ (𝐴 ∈ V → dom {{{𝐴}}} = {𝐴}) |
|
Theorem | rnsnopg 4973 |
The range of a singleton of an ordered pair is the singleton of the second
member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro,
30-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → ran {〈𝐴, 𝐵〉} = {𝐵}) |
|
Theorem | rnpropg 4974 |
The range of a pair of ordered pairs is the pair of second members.
(Contributed by Thierry Arnoux, 3-Jan-2017.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = {𝐶, 𝐷}) |
|
Theorem | rnsnop 4975 |
The range of a singleton of an ordered pair is the singleton of the
second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario
Carneiro, 26-Apr-2015.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ran {〈𝐴, 𝐵〉} = {𝐵} |
|
Theorem | op1sta 4976 |
Extract the first member of an ordered pair. (See op2nda 4979 to extract
the second member and op1stb 4357 for an alternate version.)
(Contributed
by Raph Levien, 4-Dec-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∪
dom {〈𝐴, 𝐵〉} = 𝐴 |
|
Theorem | cnvsn 4977 |
Converse of a singleton of an ordered pair. (Contributed by NM,
11-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉} |
|
Theorem | op2ndb 4978 |
Extract the second member of an ordered pair. Theorem 5.12(ii) of
[Monk1] p. 52. (See op1stb 4357 to extract the first member and op2nda 4979
for an alternate version.) (Contributed by NM, 25-Nov-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∩
∩ ∩ ◡{〈𝐴, 𝐵〉} = 𝐵 |
|
Theorem | op2nda 4979 |
Extract the second member of an ordered pair. (See op1sta 4976 to extract
the first member and op2ndb 4978 for an alternate version.) (Contributed
by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∪
ran {〈𝐴, 𝐵〉} = 𝐵 |
|
Theorem | cnvsng 4980 |
Converse of a singleton of an ordered pair. (Contributed by NM,
23-Jan-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉}) |
|
Theorem | opswapg 4981 |
Swap the members of an ordered pair. (Contributed by Jim Kingdon,
16-Dec-2018.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ ◡{〈𝐴, 𝐵〉} = 〈𝐵, 𝐴〉) |
|
Theorem | elxp4 4982 |
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp5 4983. (Contributed by NM,
17-Feb-2004.)
|
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∪ dom
{𝐴}, ∪ ran {𝐴}〉 ∧ (∪
dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) |
|
Theorem | elxp5 4983 |
Membership in a cross product requiring no quantifiers or dummy
variables. Provides a slightly shorter version of elxp4 4982 when the
double intersection does not create class existence problems (caused by
int0 3749). (Contributed by NM, 1-Aug-2004.)
|
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∩ ∩ 𝐴,
∪ ran {𝐴}〉 ∧ (∩
∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
|
Theorem | cnvresima 4984 |
An image under the converse of a restriction. (Contributed by Jeff
Hankins, 12-Jul-2009.)
|
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴) |
|
Theorem | resdm2 4985 |
A class restricted to its domain equals its double converse. (Contributed
by NM, 8-Apr-2007.)
|
⊢ (𝐴 ↾ dom 𝐴) = ◡◡𝐴 |
|
Theorem | resdmres 4986 |
Restriction to the domain of a restriction. (Contributed by NM,
8-Apr-2007.)
|
⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵) |
|
Theorem | imadmres 4987 |
The image of the domain of a restriction. (Contributed by NM,
8-Apr-2007.)
|
⊢ (𝐴 “ dom (𝐴 ↾ 𝐵)) = (𝐴 “ 𝐵) |
|
Theorem | mptpreima 4988* |
The preimage of a function in maps-to notation. (Contributed by Stefan
O'Rear, 25-Jan-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} |
|
Theorem | mptiniseg 4989* |
Converse singleton image of a function defined by maps-to. (Contributed
by Stefan O'Rear, 25-Jan-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑉 → (◡𝐹 “ {𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶}) |
|
Theorem | dmmpt 4990 |
The domain of the mapping operation in general. (Contributed by NM,
16-May-1995.) (Revised by Mario Carneiro, 22-Mar-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} |
|
Theorem | dmmptss 4991* |
The domain of a mapping is a subset of its base class. (Contributed by
Scott Fenton, 17-Jun-2013.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 |
|
Theorem | dmmptg 4992* |
The domain of the mapping operation is the stated domain, if the
function value is always a set. (Contributed by Mario Carneiro,
9-Feb-2013.) (Revised by Mario Carneiro, 14-Sep-2013.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
|
Theorem | relco 4993 |
A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25.
(Contributed by NM, 26-Jan-1997.)
|
⊢ Rel (𝐴 ∘ 𝐵) |
|
Theorem | dfco2 4994* |
Alternate definition of a class composition, using only one bound
variable. (Contributed by NM, 19-Dec-2008.)
|
⊢ (𝐴 ∘ 𝐵) = ∪
𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) |
|
Theorem | dfco2a 4995* |
Generalization of dfco2 4994, where 𝐶 can have any value between
dom 𝐴 ∩ ran 𝐵 and V.
(Contributed by NM, 21-Dec-2008.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (𝐴 ∘ 𝐵) = ∪
𝑥 ∈ 𝐶 ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) |
|
Theorem | coundi 4996 |
Class composition distributes over union. (Contributed by NM,
21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶)) |
|
Theorem | coundir 4997 |
Class composition distributes over union. (Contributed by NM,
21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ ((𝐴 ∪ 𝐵) ∘ 𝐶) = ((𝐴 ∘ 𝐶) ∪ (𝐵 ∘ 𝐶)) |
|
Theorem | cores 4998 |
Restricted first member of a class composition. (Contributed by NM,
12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵)) |
|
Theorem | resco 4999 |
Associative law for the restriction of a composition. (Contributed by
NM, 12-Dec-2006.)
|
⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶)) |
|
Theorem | imaco 5000 |
Image of the composition of two classes. (Contributed by Jason
Orendorff, 12-Dec-2006.)
|
⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶)) |