![]() |
Metamath
Proof Explorer Theorem List (p. 59 of 489) | < 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: | ![]() (1-30950) |
![]() (30951-32473) |
![]() (32474-48899) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | releqi 5801 | Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (Rel 𝐴 ↔ Rel 𝐵) | ||
Theorem | releqd 5802 | Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Rel 𝐴 ↔ Rel 𝐵)) | ||
Theorem | nfrel 5803 | Bound-variable hypothesis builder for a relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥Rel 𝐴 | ||
Theorem | sbcrel 5804 | Distribute proper substitution through a relation predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Rel 𝑅 ↔ Rel ⦋𝐴 / 𝑥⦌𝑅)) | ||
Theorem | relss 5805 | Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.) |
⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴)) | ||
Theorem | ssrel 5806* | 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 5317, ax-nul 5324, ax-pr 5447. (Revised by KP, 25-Oct-2021.) Remove dependency on ax-12 2178. (Revised by SN, 11-Dec-2024.) |
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵))) | ||
Theorem | ssrelOLD 5807* | Obsolete version of ssrel 5806 as of 11-Dec-2024. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Remove dependency on ax-sep 5317, ax-nul 5324, ax-pr 5447. (Revised by KP, 25-Oct-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵))) | ||
Theorem | eqrel 5808* | Extensionality principle for relations. Theorem 3.2(ii) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) |
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵))) | ||
Theorem | ssrel2 5809* | A subclass relationship depends only on a relation's ordered pairs. This version of ssrel 5806 is restricted to the relation's domain. (Contributed by Thierry Arnoux, 25-Jan-2018.) |
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → (𝑅 ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (〈𝑥, 𝑦〉 ∈ 𝑅 → 〈𝑥, 𝑦〉 ∈ 𝑆))) | ||
Theorem | ssrel3 5810* | Subclass relation in another form when the subclass is a relation. (Contributed by Peter Mazsa, 16-Feb-2019.) |
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → 𝑥𝐵𝑦))) | ||
Theorem | relssi 5811* | Inference from subclass principle for relations. (Contributed by NM, 31-Mar-1998.) |
⊢ Rel 𝐴 & ⊢ (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵) ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
Theorem | relssdv 5812* | Deduction from subclass principle for relations. (Contributed by NM, 11-Sep-2004.) |
⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | eqrelriv 5813* | Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012.) |
⊢ (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵) ⇒ ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵) | ||
Theorem | eqrelriiv 5814* | Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995.) |
⊢ Rel 𝐴 & ⊢ Rel 𝐵 & ⊢ (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵) ⇒ ⊢ 𝐴 = 𝐵 | ||
Theorem | eqbrriv 5815* | Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006.) |
⊢ Rel 𝐴 & ⊢ Rel 𝐵 & ⊢ (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦) ⇒ ⊢ 𝐴 = 𝐵 | ||
Theorem | eqrelrdv 5816* | Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010.) |
⊢ Rel 𝐴 & ⊢ Rel 𝐵 & ⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | eqbrrdv 5817* | Deduction from extensionality principle for relations. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → Rel 𝐵) & ⊢ (𝜑 → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | eqbrrdiv 5818* | Deduction from extensionality principle for relations. (Contributed by Rodolfo Medina, 10-Oct-2010.) |
⊢ Rel 𝐴 & ⊢ Rel 𝐵 & ⊢ (𝜑 → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | eqrelrdv2 5819* | A version of eqrelrdv 5816. (Contributed by Rodolfo Medina, 10-Oct-2010.) |
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵)) ⇒ ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵) | ||
Theorem | ssrelrel 5820* | A subclass relationship determined by ordered triples. Use relrelss 6304 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 5821* | Extensionality principle for ordered triples (used by 2-place operations df-oprab 7452), analogous to eqrel 5808. Use relrelss 6304 to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008.) |
⊢ ((𝐴 ∪ 𝐵) ⊆ ((V × V) × V) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵))) | ||
Theorem | elrel 5822* | A member of a relation is an ordered pair. (Contributed by NM, 17-Sep-2006.) |
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → ∃𝑥∃𝑦 𝐴 = 〈𝑥, 𝑦〉) | ||
Theorem | rel0 5823 | The empty set is a relation. (Contributed by NM, 26-Apr-1998.) |
⊢ Rel ∅ | ||
Theorem | nrelv 5824 | The universal class is not a relation. (Contributed by Thierry Arnoux, 23-Jan-2022.) |
⊢ ¬ Rel V | ||
Theorem | relsng 5825 | 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 5826 | 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 5827 | A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998.) (Revised by BJ, 12-Feb-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Rel {〈𝐴, 𝐵〉}) | ||
Theorem | relsn 5828 | A singleton is a relation iff it is an ordered pair. (Contributed by NM, 24-Sep-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Rel {𝐴} ↔ 𝐴 ∈ (V × V)) | ||
Theorem | relsnop 5829 | 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 5830* | Implicit substitution inference for ordered pairs. Compare copsex2ga 5831. (Contributed by NM, 12-Mar-2014.) |
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ (𝐴 ∈ (V × V) ∧ 𝜑)) | ||
Theorem | copsex2ga 5831* | Implicit substitution inference for ordered pairs. Compare copsex2g 5513. (Contributed by NM, 26-Feb-2014.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ (𝑉 × 𝑊) → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜓))) | ||
Theorem | elopaba 5832* | Membership in an ordered-pair class abstraction. (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ (𝐴 ∈ (V × V) ∧ 𝜑)) | ||
Theorem | xpsspw 5833 | 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 5834 | The double class union of a Cartesian product is included in the union of its arguments. (Contributed by NM, 16-Sep-2006.) |
⊢ ∪ ∪ (𝐴 × 𝐵) ⊆ (𝐴 ∪ 𝐵) | ||
Theorem | relun 5835 | 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 5836 | The intersection with a relation is a relation. (Contributed by NM, 16-Aug-1994.) |
⊢ (Rel 𝐴 → Rel (𝐴 ∩ 𝐵)) | ||
Theorem | relin2 5837 | The intersection with a relation is a relation. (Contributed by NM, 17-Jan-2006.) |
⊢ (Rel 𝐵 → Rel (𝐴 ∩ 𝐵)) | ||
Theorem | relinxp 5838 | Intersection with a Cartesian product is a relation. (Contributed by Peter Mazsa, 4-Mar-2019.) |
⊢ Rel (𝑅 ∩ (𝐴 × 𝐵)) | ||
Theorem | reldif 5839 | A difference cutting down a relation is a relation. (Contributed by NM, 31-Mar-1998.) |
⊢ (Rel 𝐴 → Rel (𝐴 ∖ 𝐵)) | ||
Theorem | reliun 5840 | 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 5841 | 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 5842* | 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 5843* | 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 5844* | A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2158 and ax-12 2178, see relopabi 5846. (Contributed by BJ, 22-Jul-2023.) |
⊢ 𝐴 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ Rel 𝐴 | ||
Theorem | relopabv 5845* | A class of ordered pairs is a relation. For a version without a disjoint variable condition, but using ax-11 2158 and ax-12 2178, see relopab 5848. (Contributed by SN, 8-Sep-2024.) |
⊢ Rel {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | relopabi 5846 | A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.) Remove dependency on ax-sep 5317, ax-nul 5324, ax-pr 5447. (Revised by KP, 25-Oct-2021.) |
⊢ 𝐴 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ Rel 𝐴 | ||
Theorem | relopabiALT 5847 | Alternate proof of relopabi 5846 (shorter but uses more axioms). (Contributed by Mario Carneiro, 21-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ Rel 𝐴 | ||
Theorem | relopab 5848 | 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 5849 | The maps-to notation always describes a binary relation. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ Rel (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | reli 5850 | 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 5851 | The membership relation is a relation. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.) |
⊢ Rel E | ||
Theorem | opabid2 5852* | A relation expressed as an ordered pair abstraction. (Contributed by NM, 11-Dec-2006.) |
⊢ (Rel 𝐴 → {〈𝑥, 𝑦〉 ∣ 〈𝑥, 𝑦〉 ∈ 𝐴} = 𝐴) | ||
Theorem | inopab 5853* | Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | difopab 5854* | Difference of two ordered-pair class abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Proof shortened by SN, 19-Dec-2024.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∖ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ ¬ 𝜓)} | ||
Theorem | difopabOLD 5855* | Obsolete version of difopab 5854 as of 19-Dec-2024. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∖ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ ¬ 𝜓)} | ||
Theorem | inxp 5856 | 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.) Avoid ax-10 2141, ax-12 2178. (Revised by SN, 5-May-2025.) |
⊢ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷)) | ||
Theorem | inxpOLD 5857 | Obsolete version of inxp 5856 as of 5-May-2025. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷)) | ||
Theorem | xpindi 5858 | Distributive law for Cartesian product over intersection. Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.) |
⊢ (𝐴 × (𝐵 ∩ 𝐶)) = ((𝐴 × 𝐵) ∩ (𝐴 × 𝐶)) | ||
Theorem | xpindir 5859 | Distributive law for Cartesian product over intersection. Similar to Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.) |
⊢ ((𝐴 ∩ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∩ (𝐵 × 𝐶)) | ||
Theorem | xpiindi 5860* | Distributive law for Cartesian product over indexed intersection. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐴 ≠ ∅ → (𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) = ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) | ||
Theorem | xpriindi 5861* | Distributive law for Cartesian product over relativized indexed intersection. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐶 × (𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵)) = ((𝐶 × 𝐷) ∩ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) | ||
Theorem | eliunxp 5862* | Membership in a union of Cartesian products. Analogue of elxp 5723 for nonconstant 𝐵(𝑥). (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | ||
Theorem | opeliunxp2 5863* | Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸) ⇒ ⊢ (〈𝐶, 𝐷〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) | ||
Theorem | raliunxp 5864* | Write a double restricted quantification as one universal quantifier. In this version of ralxp 5866, 𝐵(𝑦) is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) | ||
Theorem | rexiunxp 5865* | Write a double restricted quantification as one universal quantifier. In this version of rexxp 5867, 𝐵(𝑦) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) | ||
Theorem | ralxp 5866* | 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 5867* | 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 5868* | 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 5869* | Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014.) |
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (Rel 𝐴 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑧(〈𝑦, 𝑧〉 ∈ 𝐴 ∧ 𝜓))) | ||
Theorem | djussxp 5870* | Disjoint union is a subset of a Cartesian product. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V) | ||
Theorem | ralxpf 5871* | Version of ralxp 5866 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) | ||
Theorem | rexxpf 5872* | Version of rexxp 5867 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) | ||
Theorem | iunxpf 5873* | Indexed union on a Cartesian product equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008.) |
⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ (𝑥 = 〈𝑦, 𝑧〉 → 𝐶 = 𝐷) ⇒ ⊢ ∪ 𝑥 ∈ (𝐴 × 𝐵)𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑧 ∈ 𝐵 𝐷 | ||
Theorem | opabbi2dv 5874* | Deduce equality of a relation and an ordered-pair class abstraction. Compare eqabdv 2878. (Contributed by NM, 24-Feb-2014.) |
⊢ Rel 𝐴 & ⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝐴 = {〈𝑥, 𝑦〉 ∣ 𝜓}) | ||
Theorem | relop 5875* | A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008.) A relation is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a relation is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is relsnopg 5827, as funsng 6629 is to funop 7183. (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (Rel 〈𝐴, 𝐵〉 ↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) | ||
Theorem | ideqg 5876 | 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 5877 | For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵) | ||
Theorem | ididg 5878 | A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴) | ||
Theorem | issetid 5879 | 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 5880 | Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) | ||
Theorem | coss2 5881 | Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵)) | ||
Theorem | coeq1 5882 | Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | ||
Theorem | coeq2 5883 | Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) | ||
Theorem | coeq1i 5884 | Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) | ||
Theorem | coeq2i 5885 | Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) | ||
Theorem | coeq1d 5886 | Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | ||
Theorem | coeq2d 5887 | Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) | ||
Theorem | coeq12i 5888 | Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷) | ||
Theorem | coeq12d 5889 | Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷)) | ||
Theorem | nfco 5890 | Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∘ 𝐵) | ||
Theorem | brcog 5891* | Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))) | ||
Theorem | opelco2g 5892* | Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐷 ∧ 〈𝑥, 𝐵〉 ∈ 𝐶))) | ||
Theorem | brcogw 5893 | Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍) ∧ (𝐴𝐷𝑋 ∧ 𝑋𝐶𝐵)) → 𝐴(𝐶 ∘ 𝐷)𝐵) | ||
Theorem | eqbrrdva 5894* | Deduction from extensionality principle for relations, given an equivalence only on the relation domain and range. (Contributed by Thierry Arnoux, 28-Nov-2017.) |
⊢ (𝜑 → 𝐴 ⊆ (𝐶 × 𝐷)) & ⊢ (𝜑 → 𝐵 ⊆ (𝐶 × 𝐷)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | brco 5895* | Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) | ||
Theorem | opelco 5896* | Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) | ||
Theorem | cnvss 5897 | Subset theorem for converse. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Kyle Wyonch, 27-Apr-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | ||
Theorem | cnveq 5898 | Equality theorem for converse relation. (Contributed by NM, 13-Aug-1995.) |
⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) | ||
Theorem | cnveqi 5899 | Equality inference for converse relation. (Contributed by NM, 23-Dec-2008.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ◡𝐴 = ◡𝐵 | ||
Theorem | cnveqd 5900 | Equality deduction for converse relation. (Contributed by NM, 6-Dec-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ◡𝐴 = ◡𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |