Theorem List for Intuitionistic Logic Explorer - 4601-4700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | elvv 4601* |
Membership in universal class of ordered pairs. (Contributed by NM,
4-Jul-1994.)
|
⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦 𝐴 = 〈𝑥, 𝑦〉) |
|
Theorem | elvvv 4602* |
Membership in universal class of ordered triples. (Contributed by NM,
17-Dec-2008.)
|
⊢ (𝐴 ∈ ((V × V) × V) ↔
∃𝑥∃𝑦∃𝑧 𝐴 = 〈〈𝑥, 𝑦〉, 𝑧〉) |
|
Theorem | elvvuni 4603 |
An ordered pair contains its union. (Contributed by NM,
16-Sep-2006.)
|
⊢ (𝐴 ∈ (V × V) → ∪ 𝐴
∈ 𝐴) |
|
Theorem | mosubopt 4604* |
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28-Aug-2007.)
|
⊢ (∀𝑦∀𝑧∃*𝑥𝜑 → ∃*𝑥∃𝑦∃𝑧(𝐴 = 〈𝑦, 𝑧〉 ∧ 𝜑)) |
|
Theorem | mosubop 4605* |
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28-May-1995.)
|
⊢ ∃*𝑥𝜑 ⇒ ⊢ ∃*𝑥∃𝑦∃𝑧(𝐴 = 〈𝑦, 𝑧〉 ∧ 𝜑) |
|
Theorem | brinxp2 4606 |
Intersection of binary relation with cross product. (Contributed by NM,
3-Mar-2007.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴(𝑅 ∩ (𝐶 × 𝐷))𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵)) |
|
Theorem | brinxp 4607 |
Intersection of binary relation with cross product. (Contributed by NM,
9-Mar-1997.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝑅𝐵 ↔ 𝐴(𝑅 ∩ (𝐶 × 𝐷))𝐵)) |
|
Theorem | poinxp 4608 |
Intersection of partial order with cross product of its field.
(Contributed by Mario Carneiro, 10-Jul-2014.)
|
⊢ (𝑅 Po 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) Po 𝐴) |
|
Theorem | soinxp 4609 |
Intersection of linear order with cross product of its field.
(Contributed by Mario Carneiro, 10-Jul-2014.)
|
⊢ (𝑅 Or 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) Or 𝐴) |
|
Theorem | seinxp 4610 |
Intersection of set-like relation with cross product of its field.
(Contributed by Mario Carneiro, 22-Jun-2015.)
|
⊢ (𝑅 Se 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) Se 𝐴) |
|
Theorem | posng 4611 |
Partial ordering of a singleton. (Contributed by Jim Kingdon,
5-Dec-2018.)
|
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ V) → (𝑅 Po {𝐴} ↔ ¬ 𝐴𝑅𝐴)) |
|
Theorem | sosng 4612 |
Strict linear ordering on a singleton. (Contributed by Jim Kingdon,
5-Dec-2018.)
|
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ V) → (𝑅 Or {𝐴} ↔ ¬ 𝐴𝑅𝐴)) |
|
Theorem | opabssxp 4613* |
An abstraction relation is a subset of a related cross product.
(Contributed by NM, 16-Jul-1995.)
|
⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) |
|
Theorem | brab2ga 4614* |
The law of concretion for a binary relation. See brab2a 4592 for alternate
proof. TODO: should one of them be deleted? (Contributed by Mario
Carneiro, 28-Apr-2015.) (Proof modification is discouraged.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ⇒ ⊢ (𝐴𝑅𝐵 ↔ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ 𝜓)) |
|
Theorem | optocl 4615* |
Implicit substitution of class for ordered pair. (Contributed by NM,
5-Mar-1995.)
|
⊢ 𝐷 = (𝐵 × 𝐶)
& ⊢ (〈𝑥, 𝑦〉 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝐷 → 𝜓) |
|
Theorem | 2optocl 4616* |
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12-Mar-1995.)
|
⊢ 𝑅 = (𝐶 × 𝐷)
& ⊢ (〈𝑥, 𝑦〉 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (〈𝑧, 𝑤〉 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅) → 𝜒) |
|
Theorem | 3optocl 4617* |
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12-Mar-1995.)
|
⊢ 𝑅 = (𝐷 × 𝐹)
& ⊢ (〈𝑥, 𝑦〉 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (〈𝑧, 𝑤〉 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (〈𝑣, 𝑢〉 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐹) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑅) → 𝜃) |
|
Theorem | opbrop 4618* |
Ordered pair membership in a relation. Special case. (Contributed by
NM, 5-Aug-1995.)
|
⊢ (((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ (𝑣 = 𝐶 ∧ 𝑢 = 𝐷)) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ 𝜑))} ⇒ ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈𝐴, 𝐵〉𝑅〈𝐶, 𝐷〉 ↔ 𝜓)) |
|
Theorem | 0xp 4619 |
The cross product with the empty set is empty. Part of Theorem 3.13(ii)
of [Monk1] p. 37. (Contributed by NM,
4-Jul-1994.)
|
⊢ (∅ × 𝐴) = ∅ |
|
Theorem | csbxpg 4620 |
Distribute proper substitution through the cross product of two classes.
(Contributed by Alan Sare, 10-Nov-2012.)
|
⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | releq 4621 |
Equality theorem for the relation predicate. (Contributed by NM,
1-Aug-1994.)
|
⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵)) |
|
Theorem | releqi 4622 |
Equality inference for the relation predicate. (Contributed by NM,
8-Dec-2006.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (Rel 𝐴 ↔ Rel 𝐵) |
|
Theorem | releqd 4623 |
Equality deduction for the relation predicate. (Contributed by NM,
8-Mar-2014.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Rel 𝐴 ↔ Rel 𝐵)) |
|
Theorem | nfrel 4624 |
Bound-variable hypothesis builder for a relation. (Contributed by NM,
31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥Rel 𝐴 |
|
Theorem | sbcrel 4625 |
Distribute proper substitution through a relation predicate. (Contributed
by Alexander van der Vekens, 23-Jul-2017.)
|
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Rel 𝑅 ↔ Rel ⦋𝐴 / 𝑥⦌𝑅)) |
|
Theorem | relss 4626 |
Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58.
(Contributed by NM, 15-Aug-1994.)
|
⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴)) |
|
Theorem | ssrel 4627* |
A subclass relationship depends only on a relation's ordered pairs.
Theorem 3.2(i) of [Monk1] p. 33.
(Contributed by NM, 2-Aug-1994.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵))) |
|
Theorem | eqrel 4628* |
Extensionality principle for relations. Theorem 3.2(ii) of [Monk1]
p. 33. (Contributed by NM, 2-Aug-1994.)
|
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵))) |
|
Theorem | ssrel2 4629* |
A subclass relationship depends only on a relation's ordered pairs.
This version of ssrel 4627 is restricted to the relation's domain.
(Contributed by Thierry Arnoux, 25-Jan-2018.)
|
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → (𝑅 ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (〈𝑥, 𝑦〉 ∈ 𝑅 → 〈𝑥, 𝑦〉 ∈ 𝑆))) |
|
Theorem | relssi 4630* |
Inference from subclass principle for relations. (Contributed by NM,
31-Mar-1998.)
|
⊢ Rel 𝐴
& ⊢ (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵) ⇒ ⊢ 𝐴 ⊆ 𝐵 |
|
Theorem | relssdv 4631* |
Deduction from subclass principle for relations. (Contributed by NM,
11-Sep-2004.)
|
⊢ (𝜑 → Rel 𝐴)
& ⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
|
Theorem | eqrelriv 4632* |
Inference from extensionality principle for relations. (Contributed by
FL, 15-Oct-2012.)
|
⊢ (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵) ⇒ ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵) |
|
Theorem | eqrelriiv 4633* |
Inference from extensionality principle for relations. (Contributed by
NM, 17-Mar-1995.)
|
⊢ Rel 𝐴
& ⊢ Rel 𝐵
& ⊢ (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵) ⇒ ⊢ 𝐴 = 𝐵 |
|
Theorem | eqbrriv 4634* |
Inference from extensionality principle for relations. (Contributed by
NM, 12-Dec-2006.)
|
⊢ Rel 𝐴
& ⊢ Rel 𝐵
& ⊢ (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦) ⇒ ⊢ 𝐴 = 𝐵 |
|
Theorem | eqrelrdv 4635* |
Deduce equality of relations from equivalence of membership.
(Contributed by Rodolfo Medina, 10-Oct-2010.)
|
⊢ Rel 𝐴
& ⊢ Rel 𝐵
& ⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | eqbrrdv 4636* |
Deduction from extensionality principle for relations. (Contributed by
Mario Carneiro, 3-Jan-2017.)
|
⊢ (𝜑 → Rel 𝐴)
& ⊢ (𝜑 → Rel 𝐵)
& ⊢ (𝜑 → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | eqbrrdiv 4637* |
Deduction from extensionality principle for relations. (Contributed by
Rodolfo Medina, 10-Oct-2010.)
|
⊢ Rel 𝐴
& ⊢ Rel 𝐵
& ⊢ (𝜑 → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | eqrelrdv2 4638* |
A version of eqrelrdv 4635. (Contributed by Rodolfo Medina,
10-Oct-2010.)
|
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵)) ⇒ ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵) |
|
Theorem | ssrelrel 4639* |
A subclass relationship determined by ordered triples. Use relrelss 5065
to express the antecedent in terms of the relation predicate.
(Contributed by NM, 17-Dec-2008.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
⊢ (𝐴 ⊆ ((V × V) × V) →
(𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵))) |
|
Theorem | eqrelrel 4640* |
Extensionality principle for ordered triples, analogous to eqrel 4628.
Use relrelss 5065 to express the antecedent in terms of the
relation
predicate. (Contributed by NM, 17-Dec-2008.)
|
⊢ ((𝐴 ∪ 𝐵) ⊆ ((V × V) × V) →
(𝐴 = 𝐵 ↔ ∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵))) |
|
Theorem | elrel 4641* |
A member of a relation is an ordered pair. (Contributed by NM,
17-Sep-2006.)
|
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → ∃𝑥∃𝑦 𝐴 = 〈𝑥, 𝑦〉) |
|
Theorem | relsng 4642 |
A singleton is a relation iff it is an ordered pair. (Contributed by NM,
24-Sep-2013.) (Revised by BJ, 12-Feb-2022.)
|
⊢ (𝐴 ∈ 𝑉 → (Rel {𝐴} ↔ 𝐴 ∈ (V × V))) |
|
Theorem | relsnopg 4643 |
A singleton of an ordered pair is a relation. (Contributed by NM,
17-May-1998.) (Revised by BJ, 12-Feb-2022.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Rel {〈𝐴, 𝐵〉}) |
|
Theorem | relsn 4644 |
A singleton is a relation iff it is an ordered pair. (Contributed by
NM, 24-Sep-2013.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (Rel {𝐴} ↔ 𝐴 ∈ (V × V)) |
|
Theorem | relsnop 4645 |
A singleton of an ordered pair is a relation. (Contributed by NM,
17-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ Rel {〈𝐴, 𝐵〉} |
|
Theorem | xpss12 4646 |
Subset theorem for cross product. Generalization of Theorem 101 of
[Suppes] p. 52. (Contributed by NM,
26-Aug-1995.) (Proof shortened by
Andrew Salmon, 27-Aug-2011.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷)) |
|
Theorem | xpss 4647 |
A cross product is included in the ordered pair universe. Exercise 3 of
[TakeutiZaring] p. 25. (Contributed
by NM, 2-Aug-1994.)
|
⊢ (𝐴 × 𝐵) ⊆ (V × V) |
|
Theorem | relxp 4648 |
A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37.
(Contributed by NM, 2-Aug-1994.)
|
⊢ Rel (𝐴 × 𝐵) |
|
Theorem | xpss1 4649 |
Subset relation for cross product. (Contributed by Jeff Hankins,
30-Aug-2009.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶)) |
|
Theorem | xpss2 4650 |
Subset relation for cross product. (Contributed by Jeff Hankins,
30-Aug-2009.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵)) |
|
Theorem | xpsspw 4651 |
A cross product is included in the power of the power of the union of
its arguments. (Contributed by NM, 13-Sep-2006.)
|
⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) |
|
Theorem | unixpss 4652 |
The double class union of a cross product is included in the union of its
arguments. (Contributed by NM, 16-Sep-2006.)
|
⊢ ∪ ∪ (𝐴
× 𝐵) ⊆ (𝐴 ∪ 𝐵) |
|
Theorem | xpexg 4653 |
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. (Contributed
by NM, 14-Aug-1994.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
|
Theorem | xpex 4654 |
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23.
(Contributed by NM, 14-Aug-1994.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴 × 𝐵) ∈ V |
|
Theorem | sqxpexg 4655 |
The Cartesian square of a set is a set. (Contributed by AV,
13-Jan-2020.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V) |
|
Theorem | relun 4656 |
The union of two relations is a relation. Compare Exercise 5 of
[TakeutiZaring] p. 25. (Contributed
by NM, 12-Aug-1994.)
|
⊢ (Rel (𝐴 ∪ 𝐵) ↔ (Rel 𝐴 ∧ Rel 𝐵)) |
|
Theorem | relin1 4657 |
The intersection with a relation is a relation. (Contributed by NM,
16-Aug-1994.)
|
⊢ (Rel 𝐴 → Rel (𝐴 ∩ 𝐵)) |
|
Theorem | relin2 4658 |
The intersection with a relation is a relation. (Contributed by NM,
17-Jan-2006.)
|
⊢ (Rel 𝐵 → Rel (𝐴 ∩ 𝐵)) |
|
Theorem | reldif 4659 |
A difference cutting down a relation is a relation. (Contributed by NM,
31-Mar-1998.)
|
⊢ (Rel 𝐴 → Rel (𝐴 ∖ 𝐵)) |
|
Theorem | reliun 4660 |
An indexed union is a relation iff each member of its indexed family is
a relation. (Contributed by NM, 19-Dec-2008.)
|
⊢ (Rel ∪
𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 Rel 𝐵) |
|
Theorem | reliin 4661 |
An indexed intersection is a relation if at least one of the member of the
indexed family is a relation. (Contributed by NM, 8-Mar-2014.)
|
⊢ (∃𝑥 ∈ 𝐴 Rel 𝐵 → Rel ∩ 𝑥 ∈ 𝐴 𝐵) |
|
Theorem | reluni 4662* |
The union of a class is a relation iff any member is a relation.
Exercise 6 of [TakeutiZaring] p.
25 and its converse. (Contributed by
NM, 13-Aug-2004.)
|
⊢ (Rel ∪ 𝐴 ↔ ∀𝑥 ∈ 𝐴 Rel 𝑥) |
|
Theorem | relint 4663* |
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 4664 |
The empty set is a relation. (Contributed by NM, 26-Apr-1998.)
|
⊢ Rel ∅ |
|
Theorem | relopabi 4665 |
A class of ordered pairs is a relation. (Contributed by Mario Carneiro,
21-Dec-2013.)
|
⊢ 𝐴 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ Rel 𝐴 |
|
Theorem | relopab 4666 |
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 4667 |
The maps-to notation always describes a relationship. (Contributed by
Scott Fenton, 16-Apr-2012.)
|
⊢ Rel (𝑥 ∈ 𝐴 ↦ 𝐵) |
|
Theorem | reli 4668 |
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 4669 |
The membership relation is a relation. (Contributed by NM,
26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
⊢ Rel E |
|
Theorem | opabid2 4670* |
A relation expressed as an ordered pair abstraction. (Contributed by
NM, 11-Dec-2006.)
|
⊢ (Rel 𝐴 → {〈𝑥, 𝑦〉 ∣ 〈𝑥, 𝑦〉 ∈ 𝐴} = 𝐴) |
|
Theorem | inopab 4671* |
Intersection of two ordered pair class abstractions. (Contributed by
NM, 30-Sep-2002.)
|
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} |
|
Theorem | difopab 4672* |
The difference of two ordered-pair abstractions. (Contributed by Stefan
O'Rear, 17-Jan-2015.)
|
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∖ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ ¬ 𝜓)} |
|
Theorem | inxp 4673 |
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 4674 |
Distributive law for cross product over intersection. Theorem 102 of
[Suppes] p. 52. (Contributed by NM,
26-Sep-2004.)
|
⊢ (𝐴 × (𝐵 ∩ 𝐶)) = ((𝐴 × 𝐵) ∩ (𝐴 × 𝐶)) |
|
Theorem | xpindir 4675 |
Distributive law for cross product over intersection. Similar to
Theorem 102 of [Suppes] p. 52.
(Contributed by NM, 26-Sep-2004.)
|
⊢ ((𝐴 ∩ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∩ (𝐵 × 𝐶)) |
|
Theorem | xpiindim 4676* |
Distributive law for cross product over indexed intersection.
(Contributed by Jim Kingdon, 7-Dec-2018.)
|
⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) = ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |
|
Theorem | xpriindim 4677* |
Distributive law for cross product over relativized indexed
intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
|
⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝐶 × (𝐷 ∩ ∩
𝑥 ∈ 𝐴 𝐵)) = ((𝐶 × 𝐷) ∩ ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵))) |
|
Theorem | eliunxp 4678* |
Membership in a union of cross products. Analogue of elxp 4556
for
nonconstant 𝐵(𝑥). (Contributed by Mario Carneiro,
29-Dec-2014.)
|
⊢ (𝐶 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
|
Theorem | opeliunxp2 4679* |
Membership in a union of cross products. (Contributed by Mario
Carneiro, 14-Feb-2015.)
|
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸) ⇒ ⊢ (〈𝐶, 𝐷〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) |
|
Theorem | raliunxp 4680* |
Write a double restricted quantification as one universal quantifier.
In this version of ralxp 4682, 𝐵(𝑦) is not assumed to be constant.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ ∪
𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |
|
Theorem | rexiunxp 4681* |
Write a double restricted quantification as one universal quantifier.
In this version of rexxp 4683, 𝐵(𝑦) is not assumed to be constant.
(Contributed by Mario Carneiro, 14-Feb-2015.)
|
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ ∪
𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) |
|
Theorem | ralxp 4682* |
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 4683* |
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 4684* |
Disjoint union is a subset of a cross product. (Contributed by Stefan
O'Rear, 21-Nov-2014.)
|
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V) |
|
Theorem | ralxpf 4685* |
Version of ralxp 4682 with bound-variable hypotheses. (Contributed
by NM,
18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ Ⅎ𝑧𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |
|
Theorem | rexxpf 4686* |
Version of rexxp 4683 with bound-variable hypotheses. (Contributed
by NM,
19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ Ⅎ𝑧𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) |
|
Theorem | iunxpf 4687* |
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 4688* |
Deduce equality of a relation and an ordered-pair class builder.
Compare abbi2dv 2258. (Contributed by NM, 24-Feb-2014.)
|
⊢ Rel 𝐴
& ⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝐴 = {〈𝑥, 𝑦〉 ∣ 𝜓}) |
|
Theorem | relop 4689* |
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 4690 |
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 4691 |
For sets, the identity relation is the same as equality. (Contributed
by NM, 13-Aug-1995.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵) |
|
Theorem | ididg 4692 |
A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof
shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴) |
|
Theorem | issetid 4693 |
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 4694 |
Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) |
|
Theorem | coss2 4695 |
Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵)) |
|
Theorem | coeq1 4696 |
Equality theorem for composition of two classes. (Contributed by NM,
3-Jan-1997.)
|
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |
|
Theorem | coeq2 4697 |
Equality theorem for composition of two classes. (Contributed by NM,
3-Jan-1997.)
|
⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) |
|
Theorem | coeq1i 4698 |
Equality inference for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) |
|
Theorem | coeq2i 4699 |
Equality inference for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) |
|
Theorem | coeq1d 4700 |
Equality deduction for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |