Theorem List for Intuitionistic Logic Explorer - 4901-5000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | poirr2 4901 |
A partial order relation is irreflexive. (Contributed by Mario
Carneiro, 2-Nov-2015.)
|
⊢ (𝑅 Po 𝐴 → (𝑅 ∩ ( I ↾ 𝐴)) = ∅) |
|
Theorem | trinxp 4902 |
The relation induced by a transitive relation on a part of its field is
transitive. (Taking the intersection of a relation with a square cross
product is a way to restrict it to a subset of its field.) (Contributed
by FL, 31-Jul-2009.)
|
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴))) |
|
Theorem | soirri 4903 |
A strict order relation is irreflexive. (Contributed by NM,
10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|
⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ¬ 𝐴𝑅𝐴 |
|
Theorem | sotri 4904 |
A strict order relation is a transitive relation. (Contributed by NM,
10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|
⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) |
|
Theorem | son2lpi 4905 |
A strict order relation has no 2-cycle loops. (Contributed by NM,
10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|
⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ¬ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) |
|
Theorem | sotri2 4906 |
A transitivity relation. (Read ¬ B < A and B
< C implies A < C .)
(Contributed by Mario Carneiro, 10-May-2013.)
|
⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ ¬ 𝐵𝑅𝐴 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) |
|
Theorem | sotri3 4907 |
A transitivity relation. (Read A < B and ¬ C
< B implies A < C .)
(Contributed by Mario Carneiro, 10-May-2013.)
|
⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐴𝑅𝐵 ∧ ¬ 𝐶𝑅𝐵) → 𝐴𝑅𝐶) |
|
Theorem | poleloe 4908 |
Express "less than or equals" for general strict orders.
(Contributed by
Stefan O'Rear, 17-Jan-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴(𝑅 ∪ I )𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))) |
|
Theorem | poltletr 4909 |
Transitive law for general strict orders. (Contributed by Stefan O'Rear,
17-Jan-2015.)
|
⊢ ((𝑅 Po 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑅𝐵 ∧ 𝐵(𝑅 ∪ I )𝐶) → 𝐴𝑅𝐶)) |
|
Theorem | cnvopab 4910* |
The converse of a class abstraction of ordered pairs. (Contributed by
NM, 11-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ ◡{〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑦, 𝑥〉 ∣ 𝜑} |
|
Theorem | mptcnv 4911* |
The converse of a mapping function. (Contributed by Thierry Arnoux,
16-Jan-2017.)
|
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → ◡(𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐶 ↦ 𝐷)) |
|
Theorem | cnv0 4912 |
The converse of the empty set. (Contributed by NM, 6-Apr-1998.)
|
⊢ ◡∅ = ∅ |
|
Theorem | cnvi 4913 |
The converse of the identity relation. Theorem 3.7(ii) of [Monk1]
p. 36. (Contributed by NM, 26-Apr-1998.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
⊢ ◡ I
= I |
|
Theorem | cnvun 4914 |
The converse of a union is the union of converses. Theorem 16 of
[Suppes] p. 62. (Contributed by NM,
25-Mar-1998.) (Proof shortened by
Andrew Salmon, 27-Aug-2011.)
|
⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵) |
|
Theorem | cnvdif 4915 |
Distributive law for converse over set difference. (Contributed by
Mario Carneiro, 26-Jun-2014.)
|
⊢ ◡(𝐴 ∖ 𝐵) = (◡𝐴 ∖ ◡𝐵) |
|
Theorem | cnvin 4916 |
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 4917 |
Distributive law for range over union. Theorem 8 of [Suppes] p. 60.
(Contributed by NM, 24-Mar-1998.)
|
⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵) |
|
Theorem | rnin 4918 |
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 4919 |
The range of an indexed union. (Contributed by Mario Carneiro,
29-May-2015.)
|
⊢ ran ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 ran 𝐵 |
|
Theorem | rnuni 4920* |
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 4921 |
Distributive law for image over union. Theorem 35 of [Suppes] p. 65.
(Contributed by NM, 30-Sep-2002.)
|
⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) |
|
Theorem | imaundir 4922 |
The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
|
⊢ ((𝐴 ∪ 𝐵) “ 𝐶) = ((𝐴 “ 𝐶) ∪ (𝐵 “ 𝐶)) |
|
Theorem | dminss 4923 |
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 4924 |
An upper bound for intersection with an image. Theorem 41 of [Suppes]
p. 66. (Contributed by NM, 11-Aug-2004.)
|
⊢ ((𝑅 “ 𝐴) ∩ 𝐵) ⊆ (𝑅 “ (𝐴 ∩ (◡𝑅 “ 𝐵))) |
|
Theorem | inimass 4925 |
The image of an intersection (Contributed by Thierry Arnoux,
16-Dec-2017.)
|
⊢ ((𝐴 ∩ 𝐵) “ 𝐶) ⊆ ((𝐴 “ 𝐶) ∩ (𝐵 “ 𝐶)) |
|
Theorem | inimasn 4926 |
The intersection of the image of singleton (Contributed by Thierry
Arnoux, 16-Dec-2017.)
|
⊢ (𝐶 ∈ 𝑉 → ((𝐴 ∩ 𝐵) “ {𝐶}) = ((𝐴 “ {𝐶}) ∩ (𝐵 “ {𝐶}))) |
|
Theorem | cnvxp 4927 |
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 4928 |
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 4929* |
The cross product of inhabited classes is inhabited. (Contributed by
Jim Kingdon, 11-Dec-2018.)
|
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) ↔ ∃𝑧 𝑧 ∈ (𝐴 × 𝐵)) |
|
Theorem | xpm 4930* |
The cross product of inhabited classes is inhabited. (Contributed by
Jim Kingdon, 13-Dec-2018.)
|
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) ↔ ∃𝑧 𝑧 ∈ (𝐴 × 𝐵)) |
|
Theorem | xpeq0r 4931 |
A cross product is empty if at least one member is empty. (Contributed by
Jim Kingdon, 12-Dec-2018.)
|
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅) |
|
Theorem | sqxpeq0 4932 |
A Cartesian square is empty iff its member is empty. (Contributed by Jim
Kingdon, 21-Apr-2023.)
|
⊢ ((𝐴 × 𝐴) = ∅ ↔ 𝐴 = ∅) |
|
Theorem | xpdisj1 4933 |
Cross products with disjoint sets are disjoint. (Contributed by NM,
13-Sep-2004.)
|
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 × 𝐶) ∩ (𝐵 × 𝐷)) = ∅) |
|
Theorem | xpdisj2 4934 |
Cross products with disjoint sets are disjoint. (Contributed by NM,
13-Sep-2004.)
|
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 × 𝐴) ∩ (𝐷 × 𝐵)) = ∅) |
|
Theorem | xpsndisj 4935 |
Cross products with two different singletons are disjoint. (Contributed
by NM, 28-Jul-2004.)
|
⊢ (𝐵 ≠ 𝐷 → ((𝐴 × {𝐵}) ∩ (𝐶 × {𝐷})) = ∅) |
|
Theorem | djudisj 4936* |
Disjoint unions with disjoint index sets are disjoint. (Contributed by
Stefan O'Rear, 21-Nov-2014.)
|
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐶) ∩ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝐷)) = ∅) |
|
Theorem | resdisj 4937 |
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 4938* |
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 4939 |
The domain of a cross product is a subclass of the first factor.
(Contributed by NM, 19-Mar-2007.)
|
⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 |
|
Theorem | rnxpss 4940 |
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 4941 |
Upper bound for the domain of a binary relation. (Contributed by BJ,
10-Jul-2022.)
|
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → dom 𝑅 ⊆ 𝐴) |
|
Theorem | rnxpss2 4942 |
Upper bound for the range of a binary relation. (Contributed by BJ,
10-Jul-2022.)
|
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → ran 𝑅 ⊆ 𝐵) |
|
Theorem | rnxpid 4943 |
The range of a square cross product. (Contributed by FL,
17-May-2010.)
|
⊢ ran (𝐴 × 𝐴) = 𝐴 |
|
Theorem | ssxpbm 4944* |
A cross-product subclass relationship is equivalent to the relationship
for its components. (Contributed by Jim Kingdon, 12-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ (𝐴 × 𝐵) → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷))) |
|
Theorem | ssxp1 4945* |
Cross product subset cancellation. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) ⊆ (𝐵 × 𝐶) ↔ 𝐴 ⊆ 𝐵)) |
|
Theorem | ssxp2 4946* |
Cross product subset cancellation. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) ⊆ (𝐶 × 𝐵) ↔ 𝐴 ⊆ 𝐵)) |
|
Theorem | xp11m 4947* |
The cross product of inhabited classes is one-to-one. (Contributed by
Jim Kingdon, 13-Dec-2018.)
|
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
|
Theorem | xpcanm 4948* |
Cancellation law for cross-product. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) = (𝐶 × 𝐵) ↔ 𝐴 = 𝐵)) |
|
Theorem | xpcan2m 4949* |
Cancellation law for cross-product. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) = (𝐵 × 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | xpexr2m 4950* |
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 4951 |
Subset of the range of a restriction. (Contributed by NM,
16-Jan-2006.)
|
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵) |
|
Theorem | rninxp 4952* |
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 4953* |
Domain of the intersection with a cross product. (Contributed by NM,
17-Jan-2006.)
|
⊢ (dom (𝐶 ∩ (𝐴 × 𝐵)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥𝐶𝑦) |
|
Theorem | imainrect 4954 |
Image of a relation restricted to a rectangular region. (Contributed by
Stefan O'Rear, 19-Feb-2015.)
|
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) “ 𝑌) = ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵) |
|
Theorem | xpima1 4955 |
The image by a cross product. (Contributed by Thierry Arnoux,
16-Dec-2017.)
|
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅) |
|
Theorem | xpima2m 4956* |
The image by a cross product. (Contributed by Thierry Arnoux,
16-Dec-2017.)
|
⊢ (∃𝑥 𝑥 ∈ (𝐴 ∩ 𝐶) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵) |
|
Theorem | xpimasn 4957 |
The image of a singleton by a cross product. (Contributed by Thierry
Arnoux, 14-Jan-2018.)
|
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) |
|
Theorem | cnvcnv3 4958* |
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 4959 |
Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25.
(Contributed by NM, 29-Dec-1996.)
|
⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅) |
|
Theorem | dfrel4v 4960* |
A relation can be expressed as the set of ordered pairs in it.
(Contributed by Mario Carneiro, 16-Aug-2015.)
|
⊢ (Rel 𝑅 ↔ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦}) |
|
Theorem | cnvcnv 4961 |
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 4962 |
The double converse of a class equals its restriction to the universe.
(Contributed by NM, 8-Oct-2007.)
|
⊢ ◡◡𝐴 = (𝐴 ↾ V) |
|
Theorem | cnvcnvss 4963 |
The double converse of a class is a subclass. Exercise 2 of
[TakeutiZaring] p. 25. (Contributed
by NM, 23-Jul-2004.)
|
⊢ ◡◡𝐴 ⊆ 𝐴 |
|
Theorem | cnveqb 4964 |
Equality theorem for converse. (Contributed by FL, 19-Sep-2011.)
|
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ◡𝐴 = ◡𝐵)) |
|
Theorem | cnveq0 4965 |
A relation empty iff its converse is empty. (Contributed by FL,
19-Sep-2011.)
|
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ◡𝐴 = ∅)) |
|
Theorem | dfrel3 4966 |
Alternate definition of relation. (Contributed by NM, 14-May-2008.)
|
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅) |
|
Theorem | dmresv 4967 |
The domain of a universal restriction. (Contributed by NM,
14-May-2008.)
|
⊢ dom (𝐴 ↾ V) = dom 𝐴 |
|
Theorem | rnresv 4968 |
The range of a universal restriction. (Contributed by NM,
14-May-2008.)
|
⊢ ran (𝐴 ↾ V) = ran 𝐴 |
|
Theorem | dfrn4 4969 |
Range defined in terms of image. (Contributed by NM, 14-May-2008.)
|
⊢ ran 𝐴 = (𝐴 “ V) |
|
Theorem | csbrng 4970 |
Distribute proper substitution through the range of a class.
(Contributed by Alan Sare, 10-Nov-2012.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵) |
|
Theorem | rescnvcnv 4971 |
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 4972 |
The double converse of the restriction of a class. (Contributed by NM,
3-Jun-2007.)
|
⊢ ◡◡(𝐴 ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵) |
|
Theorem | imacnvcnv 4973 |
The image of the double converse of a class. (Contributed by NM,
8-Apr-2007.)
|
⊢ (◡◡𝐴 “ 𝐵) = (𝐴 “ 𝐵) |
|
Theorem | dmsnm 4974* |
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 4975* |
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 4976 |
The domain of the singleton of the empty set is empty. (Contributed by
NM, 30-Jan-2004.)
|
⊢ dom {∅} = ∅ |
|
Theorem | cnvsn0 4977 |
The converse of the singleton of the empty set is empty. (Contributed by
Mario Carneiro, 30-Aug-2015.)
|
⊢ ◡{∅} = ∅ |
|
Theorem | dmsn0el 4978 |
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 4979* |
A singleton is a relation iff it has an inhabited domain. (Contributed
by Jim Kingdon, 16-Dec-2018.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (Rel {𝐴} ↔ ∃𝑥 𝑥 ∈ dom {𝐴}) |
|
Theorem | dmsnopg 4980 |
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 4981 |
The domain of an unordered pair of ordered pairs. (Contributed by Mario
Carneiro, 26-Apr-2015.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶}) |
|
Theorem | dmsnop 4982 |
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 4983 |
The domain of an unordered pair of ordered pairs. (Contributed by NM,
13-Sep-2011.)
|
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶} |
|
Theorem | dmtpop 4984 |
The domain of an unordered triple of ordered pairs. (Contributed by NM,
14-Sep-2011.)
|
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐹 ∈
V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉} = {𝐴, 𝐶, 𝐸} |
|
Theorem | cnvcnvsn 4985 |
Double converse of a singleton of an ordered pair. (Unlike cnvsn 4991,
this does not need any sethood assumptions on 𝐴 and 𝐵.)
(Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ ◡◡{〈𝐴, 𝐵〉} = ◡{〈𝐵, 𝐴〉} |
|
Theorem | dmsnsnsng 4986 |
The domain of the singleton of the singleton of a singleton.
(Contributed by Jim Kingdon, 16-Dec-2018.)
|
⊢ (𝐴 ∈ V → dom {{{𝐴}}} = {𝐴}) |
|
Theorem | rnsnopg 4987 |
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 4988 |
The range of a pair of ordered pairs is the pair of second members.
(Contributed by Thierry Arnoux, 3-Jan-2017.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = {𝐶, 𝐷}) |
|
Theorem | rnsnop 4989 |
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 4990 |
Extract the first member of an ordered pair. (See op2nda 4993 to extract
the second member and op1stb 4369 for an alternate version.)
(Contributed
by Raph Levien, 4-Dec-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∪
dom {〈𝐴, 𝐵〉} = 𝐴 |
|
Theorem | cnvsn 4991 |
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 4992 |
Extract the second member of an ordered pair. Theorem 5.12(ii) of
[Monk1] p. 52. (See op1stb 4369 to extract the first member and op2nda 4993
for an alternate version.) (Contributed by NM, 25-Nov-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∩
∩ ∩ ◡{〈𝐴, 𝐵〉} = 𝐵 |
|
Theorem | op2nda 4993 |
Extract the second member of an ordered pair. (See op1sta 4990 to extract
the first member and op2ndb 4992 for an alternate version.) (Contributed
by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∪
ran {〈𝐴, 𝐵〉} = 𝐵 |
|
Theorem | cnvsng 4994 |
Converse of a singleton of an ordered pair. (Contributed by NM,
23-Jan-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉}) |
|
Theorem | opswapg 4995 |
Swap the members of an ordered pair. (Contributed by Jim Kingdon,
16-Dec-2018.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ ◡{〈𝐴, 𝐵〉} = 〈𝐵, 𝐴〉) |
|
Theorem | elxp4 4996 |
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp5 4997. (Contributed by NM,
17-Feb-2004.)
|
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∪ dom
{𝐴}, ∪ ran {𝐴}〉 ∧ (∪
dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) |
|
Theorem | elxp5 4997 |
Membership in a cross product requiring no quantifiers or dummy
variables. Provides a slightly shorter version of elxp4 4996 when the
double intersection does not create class existence problems (caused by
int0 3755). (Contributed by NM, 1-Aug-2004.)
|
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∩ ∩ 𝐴,
∪ ran {𝐴}〉 ∧ (∩
∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
|
Theorem | cnvresima 4998 |
An image under the converse of a restriction. (Contributed by Jeff
Hankins, 12-Jul-2009.)
|
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴) |
|
Theorem | resdm2 4999 |
A class restricted to its domain equals its double converse. (Contributed
by NM, 8-Apr-2007.)
|
⊢ (𝐴 ↾ dom 𝐴) = ◡◡𝐴 |
|
Theorem | resdmres 5000 |
Restriction to the domain of a restriction. (Contributed by NM,
8-Apr-2007.)
|
⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵) |