Home | Metamath
Proof Explorer Theorem List (p. 58 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iunxpconst 5701* | Membership in a union of Cartesian products when the second factor is constant. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵) | ||
Theorem | xpun 5702 | The Cartesian product of two unions. (Contributed by NM, 12-Aug-2004.) |
⊢ ((𝐴 ∪ 𝐵) × (𝐶 ∪ 𝐷)) = (((𝐴 × 𝐶) ∪ (𝐴 × 𝐷)) ∪ ((𝐵 × 𝐶) ∪ (𝐵 × 𝐷))) | ||
Theorem | elvv 5703* | Membership in universal class of ordered pairs. (Contributed by NM, 4-Jul-1994.) |
⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩) | ||
Theorem | elvvv 5704* | Membership in universal class of ordered triples. (Contributed by NM, 17-Dec-2008.) |
⊢ (𝐴 ∈ ((V × V) × V) ↔ ∃𝑥∃𝑦∃𝑧 𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) | ||
Theorem | elvvuni 5705 | An ordered pair contains its union. (Contributed by NM, 16-Sep-2006.) |
⊢ (𝐴 ∈ (V × V) → ∪ 𝐴 ∈ 𝐴) | ||
Theorem | brinxp2 5706 | Intersection of binary relation with Cartesian product. (Contributed by NM, 3-Mar-2007.) (Revised by Mario Carneiro, 26-Apr-2015.) Group conjuncts and avoid df-3an 1090. (Revised by Peter Mazsa, 18-Sep-2022.) |
⊢ (𝐶(𝑅 ∩ (𝐴 × 𝐵))𝐷 ↔ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) ∧ 𝐶𝑅𝐷)) | ||
Theorem | brinxp 5707 | Intersection of binary relation with Cartesian product. (Contributed by NM, 9-Mar-1997.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝑅𝐵 ↔ 𝐴(𝑅 ∩ (𝐶 × 𝐷))𝐵)) | ||
Theorem | opelinxp 5708 | Ordered pair element in an intersection with Cartesian product. (Contributed by Peter Mazsa, 21-Jul-2019.) |
⊢ (⟨𝐶, 𝐷⟩ ∈ (𝑅 ∩ (𝐴 × 𝐵)) ↔ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) ∧ ⟨𝐶, 𝐷⟩ ∈ 𝑅)) | ||
Theorem | poinxp 5709 | Intersection of partial order with Cartesian product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.) |
⊢ (𝑅 Po 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) Po 𝐴) | ||
Theorem | soinxp 5710 | Intersection of total order with Cartesian product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.) |
⊢ (𝑅 Or 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) Or 𝐴) | ||
Theorem | frinxp 5711 | Intersection of well-founded relation with Cartesian product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.) |
⊢ (𝑅 Fr 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) Fr 𝐴) | ||
Theorem | seinxp 5712 | Intersection of set-like relation with Cartesian product of its field. (Contributed by Mario Carneiro, 22-Jun-2015.) |
⊢ (𝑅 Se 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) Se 𝐴) | ||
Theorem | weinxp 5713 | Intersection of well-ordering with Cartesian product of its field. (Contributed by NM, 9-Mar-1997.) (Revised by Mario Carneiro, 10-Jul-2014.) |
⊢ (𝑅 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴) | ||
Theorem | posn 5714 | Partial ordering of a singleton. (Contributed by NM, 27-Apr-2009.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ (Rel 𝑅 → (𝑅 Po {𝐴} ↔ ¬ 𝐴𝑅𝐴)) | ||
Theorem | sosn 5715 | Strict ordering on a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ (Rel 𝑅 → (𝑅 Or {𝐴} ↔ ¬ 𝐴𝑅𝐴)) | ||
Theorem | frsn 5716 | Founded relation on a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ (Rel 𝑅 → (𝑅 Fr {𝐴} ↔ ¬ 𝐴𝑅𝐴)) | ||
Theorem | wesn 5717 | Well-ordering of a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ (Rel 𝑅 → (𝑅 We {𝐴} ↔ ¬ 𝐴𝑅𝐴)) | ||
Theorem | elopaelxp 5718* | Membership in an ordered-pair class abstraction implies membership in a Cartesian product. (Contributed by Alexander van der Vekens, 23-Jun-2018.) Avoid ax-sep 5255, ax-nul 5262, ax-pr 5383. (Revised by SN, 11-Dec-2024.) |
⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓} → 𝐴 ∈ (V × V)) | ||
Theorem | elopaelxpOLD 5719* | Obsolete version of elopaelxp 5718 as of 11-Dec-2024. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓} → 𝐴 ∈ (V × V)) | ||
Theorem | bropaex12 5720* | Two classes related by an ordered-pair class abstraction are sets. (Contributed by AV, 21-Jan-2020.) |
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜓} ⇒ ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | opabssxp 5721* | An abstraction relation is a subset of a related Cartesian product. (Contributed by NM, 16-Jul-1995.) |
⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) | ||
Theorem | brab2a 5722* | The law of concretion for a binary relation. Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ⇒ ⊢ (𝐴𝑅𝐵 ↔ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ 𝜓)) | ||
Theorem | optocl 5723* | Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995.) |
⊢ 𝐷 = (𝐵 × 𝐶) & ⊢ (⟨𝑥, 𝑦⟩ = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝐷 → 𝜓) | ||
Theorem | 2optocl 5724* | Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.) |
⊢ 𝑅 = (𝐶 × 𝐷) & ⊢ (⟨𝑥, 𝑦⟩ = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (⟨𝑧, 𝑤⟩ = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅) → 𝜒) | ||
Theorem | 3optocl 5725* | Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.) |
⊢ 𝑅 = (𝐷 × 𝐹) & ⊢ (⟨𝑥, 𝑦⟩ = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (⟨𝑧, 𝑤⟩ = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (⟨𝑣, 𝑢⟩ = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐹) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑅) → 𝜃) | ||
Theorem | opbrop 5726* | Ordered pair membership in a relation. Special case. (Contributed by NM, 5-Aug-1995.) |
⊢ (((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ (𝑣 = 𝐶 ∧ 𝑢 = 𝐷)) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ 𝜑))} ⇒ ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ 𝜓)) | ||
Theorem | 0xp 5727 | The Cartesian product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 4-Jul-1994.) |
⊢ (∅ × 𝐴) = ∅ | ||
Theorem | csbxp 5728 | Distribute proper substitution through the Cartesian product of two classes. (Contributed by Alan Sare, 10-Nov-2012.) (Revised by NM, 23-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | releq 5729 | Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵)) | ||
Theorem | releqi 5730 | Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (Rel 𝐴 ↔ Rel 𝐵) | ||
Theorem | releqd 5731 | Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Rel 𝐴 ↔ Rel 𝐵)) | ||
Theorem | nfrel 5732 | Bound-variable hypothesis builder for a relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥Rel 𝐴 | ||
Theorem | sbcrel 5733 | Distribute proper substitution through a relation predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Rel 𝑅 ↔ Rel ⦋𝐴 / 𝑥⦌𝑅)) | ||
Theorem | relss 5734 | Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.) |
⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴)) | ||
Theorem | ssrel 5735* | 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.) Remove dependency on ax-sep 5255, ax-nul 5262, ax-pr 5383. (Revised by KP, 25-Oct-2021.) Remove dependency on ax-12 2172. (Revised by SN, 11-Dec-2024.) |
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))) | ||
Theorem | ssrelOLD 5736* | Obsolete version of ssrel 5735 as of 11-Dec-2024. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Remove dependency on ax-sep 5255, ax-nul 5262, ax-pr 5383. (Revised by KP, 25-Oct-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))) | ||
Theorem | eqrel 5737* | Extensionality principle for relations. Theorem 3.2(ii) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) |
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))) | ||
Theorem | ssrel2 5738* | A subclass relationship depends only on a relation's ordered pairs. This version of ssrel 5735 is restricted to the relation's domain. (Contributed by Thierry Arnoux, 25-Jan-2018.) |
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → (𝑅 ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (⟨𝑥, 𝑦⟩ ∈ 𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))) | ||
Theorem | ssrel3 5739* | Subclass relation in another form when the subclass is a relation. (Contributed by Peter Mazsa, 16-Feb-2019.) |
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → 𝑥𝐵𝑦))) | ||
Theorem | relssi 5740* | Inference from subclass principle for relations. (Contributed by NM, 31-Mar-1998.) |
⊢ Rel 𝐴 & ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
Theorem | relssdv 5741* | Deduction from subclass principle for relations. (Contributed by NM, 11-Sep-2004.) |
⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | eqrelriv 5742* | Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012.) |
⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵) ⇒ ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵) | ||
Theorem | eqrelriiv 5743* | Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995.) |
⊢ Rel 𝐴 & ⊢ Rel 𝐵 & ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵) ⇒ ⊢ 𝐴 = 𝐵 | ||
Theorem | eqbrriv 5744* | Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006.) |
⊢ Rel 𝐴 & ⊢ Rel 𝐵 & ⊢ (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦) ⇒ ⊢ 𝐴 = 𝐵 | ||
Theorem | eqrelrdv 5745* | Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010.) |
⊢ Rel 𝐴 & ⊢ Rel 𝐵 & ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | eqbrrdv 5746* | Deduction from extensionality principle for relations. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → Rel 𝐵) & ⊢ (𝜑 → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | eqbrrdiv 5747* | Deduction from extensionality principle for relations. (Contributed by Rodolfo Medina, 10-Oct-2010.) |
⊢ Rel 𝐴 & ⊢ Rel 𝐵 & ⊢ (𝜑 → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | eqrelrdv2 5748* | A version of eqrelrdv 5745. (Contributed by Rodolfo Medina, 10-Oct-2010.) |
⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)) ⇒ ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵) | ||
Theorem | ssrelrel 5749* | A subclass relationship determined by ordered triples. Use relrelss 6222 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 5750* | Extensionality principle for ordered triples (used by 2-place operations df-oprab 7354), analogous to eqrel 5737. Use relrelss 6222 to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008.) |
⊢ ((𝐴 ∪ 𝐵) ⊆ ((V × V) × V) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦∀𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ 𝐴 ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ 𝐵))) | ||
Theorem | elrel 5751* | A member of a relation is an ordered pair. (Contributed by NM, 17-Sep-2006.) |
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → ∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩) | ||
Theorem | rel0 5752 | The empty set is a relation. (Contributed by NM, 26-Apr-1998.) |
⊢ Rel ∅ | ||
Theorem | nrelv 5753 | The universal class is not a relation. (Contributed by Thierry Arnoux, 23-Jan-2022.) |
⊢ ¬ Rel V | ||
Theorem | relsng 5754 | A singleton is a relation iff it is a singleton on an ordered pair. (Contributed by NM, 24-Sep-2013.) (Revised by BJ, 12-Feb-2022.) |
⊢ (𝐴 ∈ 𝑉 → (Rel {𝐴} ↔ 𝐴 ∈ (V × V))) | ||
Theorem | relsnb 5755 | An at-most-singleton is a relation iff it is empty (because it is a "singleton on a proper class") or it is a singleton of an ordered pair. (Contributed by BJ, 26-Feb-2023.) |
⊢ (Rel {𝐴} ↔ (¬ 𝐴 ∈ V ∨ 𝐴 ∈ (V × V))) | ||
Theorem | relsnopg 5756 | A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998.) (Revised by BJ, 12-Feb-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Rel {⟨𝐴, 𝐵⟩}) | ||
Theorem | relsn 5757 | A singleton is a relation iff it is an ordered pair. (Contributed by NM, 24-Sep-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Rel {𝐴} ↔ 𝐴 ∈ (V × V)) | ||
Theorem | relsnop 5758 | 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 | copsex2gb 5759* | Implicit substitution inference for ordered pairs. Compare copsex2ga 5760. (Contributed by NM, 12-Mar-2014.) |
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ (𝐴 ∈ (V × V) ∧ 𝜑)) | ||
Theorem | copsex2ga 5760* | Implicit substitution inference for ordered pairs. Compare copsex2g 5448. (Contributed by NM, 26-Feb-2014.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ (𝑉 × 𝑊) → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜓))) | ||
Theorem | elopaba 5761* | Membership in an ordered-pair class abstraction. (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ (𝐴 ∈ (V × V) ∧ 𝜑)) | ||
Theorem | xpsspw 5762 | A Cartesian product is included in the power of the power of the union of its arguments. (Contributed by NM, 13-Sep-2006.) |
⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | ||
Theorem | unixpss 5763 | The double class union of a Cartesian product is included in the union of its arguments. (Contributed by NM, 16-Sep-2006.) |
⊢ ∪ ∪ (𝐴 × 𝐵) ⊆ (𝐴 ∪ 𝐵) | ||
Theorem | relun 5764 | 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 5765 | The intersection with a relation is a relation. (Contributed by NM, 16-Aug-1994.) |
⊢ (Rel 𝐴 → Rel (𝐴 ∩ 𝐵)) | ||
Theorem | relin2 5766 | The intersection with a relation is a relation. (Contributed by NM, 17-Jan-2006.) |
⊢ (Rel 𝐵 → Rel (𝐴 ∩ 𝐵)) | ||
Theorem | relinxp 5767 | Intersection with a Cartesian product is a relation. (Contributed by Peter Mazsa, 4-Mar-2019.) |
⊢ Rel (𝑅 ∩ (𝐴 × 𝐵)) | ||
Theorem | reldif 5768 | A difference cutting down a relation is a relation. (Contributed by NM, 31-Mar-1998.) |
⊢ (Rel 𝐴 → Rel (𝐴 ∖ 𝐵)) | ||
Theorem | reliun 5769 | 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 5770 | 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 5771* | 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 5772* | 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 | relopabiv 5773* | A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2155 and ax-12 2172, see relopabi 5775. (Contributed by BJ, 22-Jul-2023.) |
⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⇒ ⊢ Rel 𝐴 | ||
Theorem | relopabv 5774* | A class of ordered pairs is a relation. For a version without a disjoint variable condition, but using ax-11 2155 and ax-12 2172, see relopab 5777. (Contributed by SN, 8-Sep-2024.) |
⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑} | ||
Theorem | relopabi 5775 | A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.) Remove dependency on ax-sep 5255, ax-nul 5262, ax-pr 5383. (Revised by KP, 25-Oct-2021.) |
⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⇒ ⊢ Rel 𝐴 | ||
Theorem | relopabiALT 5776 | Alternate proof of relopabi 5775 (shorter but uses more axioms). (Contributed by Mario Carneiro, 21-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⇒ ⊢ Rel 𝐴 | ||
Theorem | relopab 5777 | A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.) Remove disjoint variable conditions. (Revised by Alan Sare, 9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.) |
⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑} | ||
Theorem | mptrel 5778 | The maps-to notation always describes a binary relation. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ Rel (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | reli 5779 | 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 5780 | The membership relation is a relation. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.) |
⊢ Rel E | ||
Theorem | opabid2 5781* | A relation expressed as an ordered pair abstraction. (Contributed by NM, 11-Dec-2006.) |
⊢ (Rel 𝐴 → {⟨𝑥, 𝑦⟩ ∣ ⟨𝑥, 𝑦⟩ ∈ 𝐴} = 𝐴) | ||
Theorem | inopab 5782* | Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) |
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∩ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | difopab 5783* | Difference of two ordered-pair class abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Proof shortened by SN, 19-Dec-2024.) |
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)} | ||
Theorem | difopabOLD 5784* | Obsolete version of difopab 5783 as of 19-Dec-2024. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)} | ||
Theorem | inxp 5785 | Intersection of two Cartesian products. Exercise 9 of [TakeutiZaring] p. 25. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷)) | ||
Theorem | xpindi 5786 | Distributive law for Cartesian product over intersection. Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.) |
⊢ (𝐴 × (𝐵 ∩ 𝐶)) = ((𝐴 × 𝐵) ∩ (𝐴 × 𝐶)) | ||
Theorem | xpindir 5787 | Distributive law for Cartesian product over intersection. Similar to Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.) |
⊢ ((𝐴 ∩ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∩ (𝐵 × 𝐶)) | ||
Theorem | xpiindi 5788* | Distributive law for Cartesian product over indexed intersection. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐴 ≠ ∅ → (𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) = ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) | ||
Theorem | xpriindi 5789* | Distributive law for Cartesian product over relativized indexed intersection. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐶 × (𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵)) = ((𝐶 × 𝐷) ∩ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) | ||
Theorem | eliunxp 5790* | Membership in a union of Cartesian products. Analogue of elxp 5654 for nonconstant 𝐵(𝑥). (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥∃𝑦(𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | ||
Theorem | opeliunxp2 5791* | Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸) ⇒ ⊢ (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) | ||
Theorem | raliunxp 5792* | Write a double restricted quantification as one universal quantifier. In this version of ralxp 5794, 𝐵(𝑦) is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) | ||
Theorem | rexiunxp 5793* | Write a double restricted quantification as one universal quantifier. In this version of rexxp 5795, 𝐵(𝑦) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) | ||
Theorem | ralxp 5794* | Universal quantification restricted to a Cartesian 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 5795* | Existential quantification restricted to a Cartesian product is equivalent to a double restricted quantification. (Contributed by NM, 11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.) |
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) | ||
Theorem | exopxfr 5796* | Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ (V × V)𝜑 ↔ ∃𝑦∃𝑧𝜓) | ||
Theorem | exopxfr2 5797* | Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014.) |
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (Rel 𝐴 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑧(⟨𝑦, 𝑧⟩ ∈ 𝐴 ∧ 𝜓))) | ||
Theorem | djussxp 5798* | Disjoint union is a subset of a Cartesian product. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V) | ||
Theorem | ralxpf 5799* | Version of ralxp 5794 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) | ||
Theorem | rexxpf 5800* | Version of rexxp 5795 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |