Theorem List for Intuitionistic Logic Explorer - 4601-4700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | relint 4601* |
The intersection of a class is a relation if at least one member is a
relation. (Contributed by NM, 8-Mar-2014.)
|
⊢ (∃𝑥 ∈ 𝐴 Rel 𝑥 → Rel ∩
𝐴) |
|
Theorem | rel0 4602 |
The empty set is a relation. (Contributed by NM, 26-Apr-1998.)
|
⊢ Rel ∅ |
|
Theorem | relopabi 4603 |
A class of ordered pairs is a relation. (Contributed by Mario Carneiro,
21-Dec-2013.)
|
⊢ 𝐴 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ Rel 𝐴 |
|
Theorem | relopab 4604 |
A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.)
(Unnecessary distinct variable restrictions were removed by Alan Sare,
9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.)
|
⊢ Rel {〈𝑥, 𝑦〉 ∣ 𝜑} |
|
Theorem | mptrel 4605 |
The maps-to notation always describes a relationship. (Contributed by
Scott Fenton, 16-Apr-2012.)
|
⊢ Rel (𝑥 ∈ 𝐴 ↦ 𝐵) |
|
Theorem | reli 4606 |
The identity relation is a relation. Part of Exercise 4.12(p) of
[Mendelson] p. 235. (Contributed by
NM, 26-Apr-1998.) (Revised by
Mario Carneiro, 21-Dec-2013.)
|
⊢ Rel I |
|
Theorem | rele 4607 |
The membership relation is a relation. (Contributed by NM,
26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
⊢ Rel E |
|
Theorem | opabid2 4608* |
A relation expressed as an ordered pair abstraction. (Contributed by
NM, 11-Dec-2006.)
|
⊢ (Rel 𝐴 → {〈𝑥, 𝑦〉 ∣ 〈𝑥, 𝑦〉 ∈ 𝐴} = 𝐴) |
|
Theorem | inopab 4609* |
Intersection of two ordered pair class abstractions. (Contributed by
NM, 30-Sep-2002.)
|
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} |
|
Theorem | difopab 4610* |
The difference of two ordered-pair abstractions. (Contributed by Stefan
O'Rear, 17-Jan-2015.)
|
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∖ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ ¬ 𝜓)} |
|
Theorem | inxp 4611 |
The intersection of two cross products. Exercise 9 of [TakeutiZaring]
p. 25. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
⊢ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷)) |
|
Theorem | xpindi 4612 |
Distributive law for cross product over intersection. Theorem 102 of
[Suppes] p. 52. (Contributed by NM,
26-Sep-2004.)
|
⊢ (𝐴 × (𝐵 ∩ 𝐶)) = ((𝐴 × 𝐵) ∩ (𝐴 × 𝐶)) |
|
Theorem | xpindir 4613 |
Distributive law for cross product over intersection. Similar to
Theorem 102 of [Suppes] p. 52.
(Contributed by NM, 26-Sep-2004.)
|
⊢ ((𝐴 ∩ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∩ (𝐵 × 𝐶)) |
|
Theorem | xpiindim 4614* |
Distributive law for cross product over indexed intersection.
(Contributed by Jim Kingdon, 7-Dec-2018.)
|
⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) = ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |
|
Theorem | xpriindim 4615* |
Distributive law for cross product over relativized indexed
intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
|
⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝐶 × (𝐷 ∩ ∩
𝑥 ∈ 𝐴 𝐵)) = ((𝐶 × 𝐷) ∩ ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵))) |
|
Theorem | eliunxp 4616* |
Membership in a union of cross products. Analogue of elxp 4494
for
nonconstant 𝐵(𝑥). (Contributed by Mario Carneiro,
29-Dec-2014.)
|
⊢ (𝐶 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
|
Theorem | opeliunxp2 4617* |
Membership in a union of cross products. (Contributed by Mario
Carneiro, 14-Feb-2015.)
|
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸) ⇒ ⊢ (〈𝐶, 𝐷〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) |
|
Theorem | raliunxp 4618* |
Write a double restricted quantification as one universal quantifier.
In this version of ralxp 4620, 𝐵(𝑦) is not assumed to be constant.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ ∪
𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |
|
Theorem | rexiunxp 4619* |
Write a double restricted quantification as one universal quantifier.
In this version of rexxp 4621, 𝐵(𝑦) is not assumed to be constant.
(Contributed by Mario Carneiro, 14-Feb-2015.)
|
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ ∪
𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) |
|
Theorem | ralxp 4620* |
Universal quantification restricted to a cross product is equivalent to
a double restricted quantification. The hypothesis specifies an
implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by
Mario Carneiro, 29-Dec-2014.)
|
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |
|
Theorem | rexxp 4621* |
Existential quantification restricted to a cross product is equivalent
to a double restricted quantification. (Contributed by NM,
11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.)
|
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) |
|
Theorem | djussxp 4622* |
Disjoint union is a subset of a cross product. (Contributed by Stefan
O'Rear, 21-Nov-2014.)
|
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V) |
|
Theorem | ralxpf 4623* |
Version of ralxp 4620 with bound-variable hypotheses. (Contributed
by NM,
18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ Ⅎ𝑧𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |
|
Theorem | rexxpf 4624* |
Version of rexxp 4621 with bound-variable hypotheses. (Contributed
by NM,
19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ Ⅎ𝑧𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) |
|
Theorem | iunxpf 4625* |
Indexed union on a cross product is equals a double indexed union. The
hypothesis specifies an implicit substitution. (Contributed by NM,
19-Dec-2008.)
|
⊢ Ⅎ𝑦𝐶
& ⊢ Ⅎ𝑧𝐶
& ⊢ Ⅎ𝑥𝐷
& ⊢ (𝑥 = 〈𝑦, 𝑧〉 → 𝐶 = 𝐷) ⇒ ⊢ ∪ 𝑥 ∈ (𝐴 × 𝐵)𝐶 = ∪
𝑦 ∈ 𝐴 ∪ 𝑧 ∈ 𝐵 𝐷 |
|
Theorem | opabbi2dv 4626* |
Deduce equality of a relation and an ordered-pair class builder.
Compare abbi2dv 2218. (Contributed by NM, 24-Feb-2014.)
|
⊢ Rel 𝐴
& ⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝐴 = {〈𝑥, 𝑦〉 ∣ 𝜓}) |
|
Theorem | relop 4627* |
A necessary and sufficient condition for a Kuratowski ordered pair to be
a relation. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this
detail.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (Rel 〈𝐴, 𝐵〉 ↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) |
|
Theorem | ideqg 4628 |
For sets, the identity relation is the same as equality. (Contributed
by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)) |
|
Theorem | ideq 4629 |
For sets, the identity relation is the same as equality. (Contributed
by NM, 13-Aug-1995.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵) |
|
Theorem | ididg 4630 |
A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof
shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴) |
|
Theorem | issetid 4631 |
Two ways of expressing set existence. (Contributed by NM, 16-Feb-2008.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario
Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ∈ V ↔ 𝐴 I 𝐴) |
|
Theorem | coss1 4632 |
Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) |
|
Theorem | coss2 4633 |
Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵)) |
|
Theorem | coeq1 4634 |
Equality theorem for composition of two classes. (Contributed by NM,
3-Jan-1997.)
|
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |
|
Theorem | coeq2 4635 |
Equality theorem for composition of two classes. (Contributed by NM,
3-Jan-1997.)
|
⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) |
|
Theorem | coeq1i 4636 |
Equality inference for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) |
|
Theorem | coeq2i 4637 |
Equality inference for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) |
|
Theorem | coeq1d 4638 |
Equality deduction for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |
|
Theorem | coeq2d 4639 |
Equality deduction for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) |
|
Theorem | coeq12i 4640 |
Equality inference for composition of two classes. (Contributed by FL,
7-Jun-2012.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷) |
|
Theorem | coeq12d 4641 |
Equality deduction for composition of two classes. (Contributed by FL,
7-Jun-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷)) |
|
Theorem | nfco 4642 |
Bound-variable hypothesis builder for function value. (Contributed by
NM, 1-Sep-1999.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∘ 𝐵) |
|
Theorem | elco 4643* |
Elements of a composed relation. (Contributed by BJ, 10-Jul-2022.)
|
⊢ (𝐴 ∈ (𝑅 ∘ 𝑆) ↔ ∃𝑥∃𝑦∃𝑧(𝐴 = 〈𝑥, 𝑧〉 ∧ (𝑥𝑆𝑦 ∧ 𝑦𝑅𝑧))) |
|
Theorem | brcog 4644* |
Ordered pair membership in a composition. (Contributed by NM,
24-Feb-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))) |
|
Theorem | opelco2g 4645* |
Ordered pair membership in a composition. (Contributed by NM,
27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐷 ∧ 〈𝑥, 𝐵〉 ∈ 𝐶))) |
|
Theorem | brcogw 4646 |
Ordered pair membership in a composition. (Contributed by Thierry
Arnoux, 14-Jan-2018.)
|
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍) ∧ (𝐴𝐷𝑋 ∧ 𝑋𝐶𝐵)) → 𝐴(𝐶 ∘ 𝐷)𝐵) |
|
Theorem | eqbrrdva 4647* |
Deduction from extensionality principle for relations, given an
equivalence only on the relation's domain and range. (Contributed by
Thierry Arnoux, 28-Nov-2017.)
|
⊢ (𝜑 → 𝐴 ⊆ (𝐶 × 𝐷)) & ⊢ (𝜑 → 𝐵 ⊆ (𝐶 × 𝐷)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | brco 4648* |
Binary relation on a composition. (Contributed by NM, 21-Sep-2004.)
(Revised by Mario Carneiro, 24-Feb-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) |
|
Theorem | opelco 4649* |
Ordered pair membership in a composition. (Contributed by NM,
27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) |
|
Theorem | cnvss 4650 |
Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
|
⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) |
|
Theorem | cnveq 4651 |
Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
|
⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) |
|
Theorem | cnveqi 4652 |
Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ ◡𝐴 = ◡𝐵 |
|
Theorem | cnveqd 4653 |
Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ◡𝐴 = ◡𝐵) |
|
Theorem | elcnv 4654* |
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by NM, 24-Mar-1998.)
|
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝑦𝑅𝑥)) |
|
Theorem | elcnv2 4655* |
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by NM, 11-Aug-2004.)
|
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑦, 𝑥〉 ∈ 𝑅)) |
|
Theorem | nfcnv 4656 |
Bound-variable hypothesis builder for converse. (Contributed by NM,
31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥◡𝐴 |
|
Theorem | opelcnvg 4657 |
Ordered-pair membership in converse. (Contributed by NM, 13-May-1999.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ ◡𝑅 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅)) |
|
Theorem | brcnvg 4658 |
The converse of a binary relation swaps arguments. Theorem 11 of [Suppes]
p. 61. (Contributed by NM, 10-Oct-2005.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) |
|
Theorem | opelcnv 4659 |
Ordered-pair membership in converse. (Contributed by NM,
13-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ ◡𝑅 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅) |
|
Theorem | brcnv 4660 |
The converse of a binary relation swaps arguments. Theorem 11 of
[Suppes] p. 61. (Contributed by NM,
13-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) |
|
Theorem | csbcnvg 4661 |
Move class substitution in and out of the converse of a function.
(Contributed by Thierry Arnoux, 8-Feb-2017.)
|
⊢ (𝐴 ∈ 𝑉 → ◡⦋𝐴 / 𝑥⦌𝐹 = ⦋𝐴 / 𝑥⦌◡𝐹) |
|
Theorem | cnvco 4662 |
Distributive law of converse over class composition. Theorem 26 of
[Suppes] p. 64. (Contributed by NM,
19-Mar-1998.) (Proof shortened by
Andrew Salmon, 27-Aug-2011.)
|
⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴) |
|
Theorem | cnvuni 4663* |
The converse of a class union is the (indexed) union of the converses of
its members. (Contributed by NM, 11-Aug-2004.)
|
⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥 |
|
Theorem | dfdm3 4664* |
Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring]
p. 24. (Contributed by NM, 28-Dec-1996.)
|
⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴} |
|
Theorem | dfrn2 4665* |
Alternate definition of range. Definition 4 of [Suppes] p. 60.
(Contributed by NM, 27-Dec-1996.)
|
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} |
|
Theorem | dfrn3 4666* |
Alternate definition of range. Definition 6.5(2) of [TakeutiZaring]
p. 24. (Contributed by NM, 28-Dec-1996.)
|
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥〈𝑥, 𝑦〉 ∈ 𝐴} |
|
Theorem | elrn2g 4667* |
Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥〈𝑥, 𝐴〉 ∈ 𝐵)) |
|
Theorem | elrng 4668* |
Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)) |
|
Theorem | dfdm4 4669 |
Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
|
⊢ dom 𝐴 = ran ◡𝐴 |
|
Theorem | dfdmf 4670* |
Definition of domain, using bound-variable hypotheses instead of
distinct variable conditions. (Contributed by NM, 8-Mar-1995.)
(Revised by Mario Carneiro, 15-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑦𝐴 ⇒ ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} |
|
Theorem | csbdmg 4671 |
Distribute proper substitution through the domain of a class.
(Contributed by Jim Kingdon, 8-Dec-2018.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌dom 𝐵 = dom ⦋𝐴 / 𝑥⦌𝐵) |
|
Theorem | eldmg 4672* |
Domain membership. Theorem 4 of [Suppes] p. 59.
(Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)) |
|
Theorem | eldm2g 4673* |
Domain membership. Theorem 4 of [Suppes] p. 59.
(Contributed by NM,
27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵)) |
|
Theorem | eldm 4674* |
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
NM, 2-Apr-2004.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦) |
|
Theorem | eldm2 4675* |
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
NM, 1-Aug-1994.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵) |
|
Theorem | dmss 4676 |
Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
|
⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵) |
|
Theorem | dmeq 4677 |
Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
|
⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵) |
|
Theorem | dmeqi 4678 |
Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ dom 𝐴 = dom 𝐵 |
|
Theorem | dmeqd 4679 |
Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → dom 𝐴 = dom 𝐵) |
|
Theorem | opeldm 4680 |
Membership of first of an ordered pair in a domain. (Contributed by NM,
30-Jul-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ 𝐶 → 𝐴 ∈ dom 𝐶) |
|
Theorem | breldm 4681 |
Membership of first of a binary relation in a domain. (Contributed by
NM, 30-Jul-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) |
|
Theorem | opeldmg 4682 |
Membership of first of an ordered pair in a domain. (Contributed by Jim
Kingdon, 9-Jul-2019.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ 𝐶 → 𝐴 ∈ dom 𝐶)) |
|
Theorem | breldmg 4683 |
Membership of first of a binary relation in a domain. (Contributed by
NM, 21-Mar-2007.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) |
|
Theorem | dmun 4684 |
The domain of a union is the union of domains. Exercise 56(a) of
[Enderton] p. 65. (Contributed by NM,
12-Aug-1994.) (Proof shortened
by Andrew Salmon, 27-Aug-2011.)
|
⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵) |
|
Theorem | dmin 4685 |
The domain of an intersection belong to the intersection of domains.
Theorem 6 of [Suppes] p. 60.
(Contributed by NM, 15-Sep-2004.)
|
⊢ dom (𝐴 ∩ 𝐵) ⊆ (dom 𝐴 ∩ dom 𝐵) |
|
Theorem | dmiun 4686 |
The domain of an indexed union. (Contributed by Mario Carneiro,
26-Apr-2016.)
|
⊢ dom ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 dom 𝐵 |
|
Theorem | dmuni 4687* |
The domain of a union. Part of Exercise 8 of [Enderton] p. 41.
(Contributed by NM, 3-Feb-2004.)
|
⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥 |
|
Theorem | dmopab 4688* |
The domain of a class of ordered pairs. (Contributed by NM,
16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
⊢ dom {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑥 ∣ ∃𝑦𝜑} |
|
Theorem | dmopabss 4689* |
Upper bound for the domain of a restricted class of ordered pairs.
(Contributed by NM, 31-Jan-2004.)
|
⊢ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴 |
|
Theorem | dmopab3 4690* |
The domain of a restricted class of ordered pairs. (Contributed by NM,
31-Jan-2004.)
|
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = 𝐴) |
|
Theorem | dm0 4691 |
The domain of the empty set is empty. Part of Theorem 3.8(v) of [Monk1]
p. 36. (Contributed by NM, 4-Jul-1994.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
⊢ dom ∅ = ∅ |
|
Theorem | dmi 4692 |
The domain of the identity relation is the universe. (Contributed by
NM, 30-Apr-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ dom I = V |
|
Theorem | dmv 4693 |
The domain of the universe is the universe. (Contributed by NM,
8-Aug-2003.)
|
⊢ dom V = V |
|
Theorem | dm0rn0 4694 |
An empty domain implies an empty range. For a similar theorem for
whether the domain and range are inhabited, see dmmrnm 4696. (Contributed
by NM, 21-May-1998.)
|
⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) |
|
Theorem | reldm0 4695 |
A relation is empty iff its domain is empty. (Contributed by NM,
15-Sep-2004.)
|
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅)) |
|
Theorem | dmmrnm 4696* |
A domain is inhabited if and only if the range is inhabited.
(Contributed by Jim Kingdon, 15-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ dom 𝐴 ↔ ∃𝑦 𝑦 ∈ ran 𝐴) |
|
Theorem | dmxpm 4697* |
The domain of a cross product. Part of Theorem 3.13(x) of [Monk1]
p. 37. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐵 → dom (𝐴 × 𝐵) = 𝐴) |
|
Theorem | dmxpid 4698 |
The domain of a square Cartesian product. (Contributed by NM,
28-Jul-1995.) (Revised by Jim Kingdon, 11-Apr-2023.)
|
⊢ dom (𝐴 × 𝐴) = 𝐴 |
|
Theorem | dmxpin 4699 |
The domain of the intersection of two square Cartesian products. Unlike
dmin 4685, equality holds. (Contributed by NM,
29-Jan-2008.)
|
⊢ dom ((𝐴 × 𝐴) ∩ (𝐵 × 𝐵)) = (𝐴 ∩ 𝐵) |
|
Theorem | xpid11 4700 |
The Cartesian product of a class with itself is one-to-one. (Contributed
by NM, 5-Nov-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ ((𝐴 × 𝐴) = (𝐵 × 𝐵) ↔ 𝐴 = 𝐵) |