![]() |
Metamath
Proof Explorer Theorem List (p. 50 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | breqdi 4901 | Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶𝐴𝐷) ⇒ ⊢ (𝜑 → 𝐶𝐵𝐷) | ||
Theorem | breqan12d 4902 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | ||
Theorem | breqan12rd 4903 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | ||
Theorem | eqnbrtrd 4904 | Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → ¬ 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴𝑅𝐶) | ||
Theorem | nbrne1 4905 | Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.) |
⊢ ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑅𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | nbrne2 4906 | Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.) |
⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | eqbrtri 4907 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵𝑅𝐶 ⇒ ⊢ 𝐴𝑅𝐶 | ||
Theorem | eqbrtrd 4908 | Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrri 4909 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐴𝑅𝐶 ⇒ ⊢ 𝐵𝑅𝐶 | ||
Theorem | eqbrtrrd 4910 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐶) | ||
Theorem | breqtri 4911 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴𝑅𝐶 | ||
Theorem | breqtrd 4912 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrri 4913 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴𝑅𝐶 | ||
Theorem | breqtrrd 4914 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | 3brtr3i 4915 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ 𝐶𝑅𝐷 | ||
Theorem | 3brtr4i 4916 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ 𝐶𝑅𝐷 | ||
Theorem | 3brtr3d 4917 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) | ||
Theorem | 3brtr4d 4918 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐶 = 𝐴) & ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) | ||
Theorem | 3brtr3g 4919 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) | ||
Theorem | 3brtr4g 4920 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) | ||
Theorem | syl5eqbr 4921 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | syl5eqbrr 4922 | A chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | syl5breq 4923 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | syl5breqr 4924 | A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
⊢ 𝐴𝑅𝐵 & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | syl6eqbr 4925 | A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | syl6eqbrr 4926 | A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | syl6breq 4927 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | syl6breqr 4928 | A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | ssbrd 4929 | Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) | ||
Theorem | ssbr 4930 | Implication from a subclass relationship of binary relations. (Contributed by Peter Mazsa, 11-Nov-2019.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) | ||
Theorem | ssbri 4931 | Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷) | ||
Theorem | nfbrd 4932 | Deduction version of bound-variable hypothesis builder nfbr 4933. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝑅) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴𝑅𝐵) | ||
Theorem | nfbr 4933 | Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴𝑅𝐵 | ||
Theorem | brab1 4934* | Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.) |
⊢ (𝑥𝑅𝐴 ↔ 𝑥 ∈ {𝑧 ∣ 𝑧𝑅𝐴}) | ||
Theorem | br0 4935 | The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.) |
⊢ ¬ 𝐴∅𝐵 | ||
Theorem | brne0 4936 | If two sets are in a binary relation, the relation cannot be empty. (Contributed by Alexander van der Vekens, 7-Jul-2018.) |
⊢ (𝐴𝑅𝐵 → 𝑅 ≠ ∅) | ||
Theorem | brun 4937 | The union of two binary relations. (Contributed by NM, 21-Dec-2008.) |
⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵)) | ||
Theorem | brin 4938 | The intersection of two relations. (Contributed by FL, 7-Oct-2008.) |
⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵)) | ||
Theorem | brdif 4939 | The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.) |
⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵)) | ||
Theorem | sbcbr123 4940 | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Revised by NM, 22-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝑅⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | sbcbr 4941* | Move substitution in and out of a binary relation. (Contributed by NM, 23-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵⦋𝐴 / 𝑥⦌𝑅𝐶) | ||
Theorem | sbcbr12g 4942* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | sbcbr1g 4943* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅𝐶)) | ||
Theorem | sbcbr2g 4944* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵𝑅⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | brsymdif 4945 | Characterization of the symmetric difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ (𝐴(𝑅 △ 𝑆)𝐵 ↔ ¬ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) | ||
Theorem | brralrspcev 4946* | Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.) |
⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥) | ||
Theorem | brimralrspcev 4947* | Restricted existential specialization with a restricted universal quantifier over an implication with a relation in the antecedent, closed form. (Contributed by AV, 20-Aug-2022.) |
⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 ((𝜑 ∧ 𝐴𝑅𝐵) → 𝜓)) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝜑 ∧ 𝐴𝑅𝑥) → 𝜓)) | ||
Syntax | copab 4948 | Extend class notation to include ordered-pair class abstraction (class builder). |
class {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Definition | df-opab 4949* | Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually 𝑥 and 𝑦 are distinct, although the definition doesn't strictly require it (see dfid2 5264 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 7501. For example, 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 27864). (Contributed by NM, 4-Jul-1994.) |
⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} | ||
Theorem | opabss 4950* | The collection of ordered pairs in a class is a subclass of it. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} ⊆ 𝑅 | ||
Theorem | opabbid 4951 | Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) | ||
Theorem | opabbidv 4952* | Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) | ||
Theorem | opabbii 4953 | Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} | ||
Theorem | nfopab 4954* | Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ Ⅎ𝑧{〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | nfopab1 4955 | The first abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥{〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | nfopab2 4956 | The second abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑦{〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | cbvopab 4957* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑤〉 ∣ 𝜓} | ||
Theorem | cbvopabv 4958* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑤〉 ∣ 𝜓} | ||
Theorem | cbvopab1 4959* | Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ 𝜓} | ||
Theorem | cbvopab2 4960* | Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑧〉 ∣ 𝜓} | ||
Theorem | cbvopab1s 4961* | Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.) |
⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ [𝑧 / 𝑥]𝜑} | ||
Theorem | cbvopab1v 4962* | Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ 𝜓} | ||
Theorem | cbvopab2v 4963* | Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑧〉 ∣ 𝜓} | ||
Theorem | unopab 4964 | Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∪ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∨ 𝜓)} | ||
Syntax | cmpt 4965 | Extend the definition of a class to include maps-to notation for defining a function via a rule. |
class (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Definition | df-mpt 4966* | Define maps-to notation for defining a function via a rule. Read as "the function which maps 𝑥 (in 𝐴) to 𝐵(𝑥)". The class expression 𝐵 is the value of the function at 𝑥 and normally contains the variable 𝑥. An example is the square function for complex numbers, (𝑥 ∈ ℂ ↦ (𝑥↑2)). Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.) |
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | ||
Theorem | mpteq12f 4967 | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12dva 4968* | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12dv 4969* | An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) |
⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12df 4970 | An equality inference for the maps-to notation. Compare mpteq12dv 4969. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12 4971* | An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.) |
⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq1 4972* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | mpteq1d 4973* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | mpteq1i 4974* | An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | mpteq2ia 4975 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | mpteq2i 4976 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | mpteq12i 4977 | An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.) |
⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷) | ||
Theorem | mpteq2da 4978 | Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | ||
Theorem | mpteq2dva 4979* | Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | ||
Theorem | mpteq2dv 4980* | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | ||
Theorem | nfmpt 4981* | Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | nfmpt1 4982 | Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.) |
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | cbvmptf 4983* | Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Thierry Arnoux, 9-Mar-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | cbvmpt 4984* | Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | cbvmptv 4985* | Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | mptv 4986* | Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.) |
⊢ (𝑥 ∈ V ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ 𝑦 = 𝐵} | ||
Syntax | wtr 4987 | Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35. |
wff Tr 𝐴 | ||
Definition | df-tr 4988 | Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 5762). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4989 (which is suggestive of the word "transitive"), dftr3 4991, dftr4 4992, dftr5 4990, and (when 𝐴 is a set) unisuc 6052. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) | ||
Theorem | dftr2 4989* | An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.) |
⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) | ||
Theorem | dftr5 4990* | An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.) |
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴) | ||
Theorem | dftr3 4991* | An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴) | ||
Theorem | dftr4 4992 | An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr 𝐴 ↔ 𝐴 ⊆ 𝒫 𝐴) | ||
Theorem | treq 4993 | Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.) |
⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵)) | ||
Theorem | trel 4994 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴)) | ||
Theorem | trel3 4995 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) |
⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐴) → 𝐵 ∈ 𝐴)) | ||
Theorem | trss 4996 | An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.) (Proof shortened by JJ, 26-Jul-2021.) |
⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) | ||
Theorem | trin 4997 | The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.) |
⊢ ((Tr 𝐴 ∧ Tr 𝐵) → Tr (𝐴 ∩ 𝐵)) | ||
Theorem | tr0 4998 | The empty set is transitive. (Contributed by NM, 16-Sep-1993.) |
⊢ Tr ∅ | ||
Theorem | trv 4999 | The universe is transitive. (Contributed by NM, 14-Sep-2003.) |
⊢ Tr V | ||
Theorem | triun 5000 | An indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∪ 𝑥 ∈ 𝐴 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |