Home | Intuitionistic Logic Explorer Theorem List (p. 41 of 137) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | breqtrid 4001 | B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrrid 4002 | B chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
⊢ 𝐴𝑅𝐵 & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrdi 4003 | A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrrdi 4004 | A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrdi 4005 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrrdi 4006 | A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | ssbrd 4007 | Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) | ||
Theorem | ssbri 4008 | Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷) | ||
Theorem | nfbrd 4009 | Deduction version of bound-variable hypothesis builder nfbr 4010. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝑅) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴𝑅𝐵) | ||
Theorem | nfbr 4010 | Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴𝑅𝐵 | ||
Theorem | brab1 4011* | Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.) |
⊢ (𝑥𝑅𝐴 ↔ 𝑥 ∈ {𝑧 ∣ 𝑧𝑅𝐴}) | ||
Theorem | br0 4012 | The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.) |
⊢ ¬ 𝐴∅𝐵 | ||
Theorem | brne0 4013 | If two sets are in a binary relation, the relation cannot be empty. In fact, the relation is also inhabited, as seen at brm 4014. (Contributed by Alexander van der Vekens, 7-Jul-2018.) |
⊢ (𝐴𝑅𝐵 → 𝑅 ≠ ∅) | ||
Theorem | brm 4014* | If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.) |
⊢ (𝐴𝑅𝐵 → ∃𝑥 𝑥 ∈ 𝑅) | ||
Theorem | brun 4015 | The union of two binary relations. (Contributed by NM, 21-Dec-2008.) |
⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵)) | ||
Theorem | brin 4016 | The intersection of two relations. (Contributed by FL, 7-Oct-2008.) |
⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵)) | ||
Theorem | brdif 4017 | The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.) |
⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵)) | ||
Theorem | sbcbrg 4018 | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝑅⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | sbcbr12g 4019* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | sbcbr1g 4020* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅𝐶)) | ||
Theorem | sbcbr2g 4021* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵𝑅⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | brralrspcev 4022* | Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.) |
⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥) | ||
Theorem | brimralrspcev 4023* | 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 4024 | Extend class notation to include ordered-pair class abstraction (class builder). |
class {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Syntax | cmpt 4025 | Extend the definition of a class to include maps-to notation for defining a function via a rule. |
class (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Definition | df-opab 4026* | 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. The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by NM, 4-Jul-1994.) |
⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} | ||
Definition | df-mpt 4027* | Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from 𝑥 (in 𝐴) to 𝐵(𝑥)." The class expression 𝐵 is the value of the function at 𝑥 and normally contains the variable 𝑥. Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.) |
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | ||
Theorem | opabss 4028* | 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 4029 | 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 4030* | Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) | ||
Theorem | opabbii 4031 | Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} | ||
Theorem | nfopab 4032* | 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 4033 | 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 4034 | 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 4035* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑤〉 ∣ 𝜓} | ||
Theorem | cbvopabv 4036* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑤〉 ∣ 𝜓} | ||
Theorem | cbvopab1 4037* | 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 4038* | Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑧〉 ∣ 𝜓} | ||
Theorem | cbvopab1s 4039* | Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.) |
⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ [𝑧 / 𝑥]𝜑} | ||
Theorem | cbvopab1v 4040* | 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 4041* | Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑧〉 ∣ 𝜓} | ||
Theorem | csbopabg 4042* | Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{〈𝑦, 𝑧〉 ∣ 𝜑} = {〈𝑦, 𝑧〉 ∣ [𝐴 / 𝑥]𝜑}) | ||
Theorem | unopab 4043 | Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∪ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∨ 𝜓)} | ||
Theorem | mpteq12f 4044 | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12dva 4045* | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12dv 4046* | An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) |
⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12 4047* | An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.) |
⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq1 4048* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | mpteq1d 4049* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | mpteq2ia 4050 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | mpteq2i 4051 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | mpteq12i 4052 | An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.) |
⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷) | ||
Theorem | mpteq2da 4053 | 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 4054* | Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | ||
Theorem | mpteq2dv 4055* | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | ||
Theorem | nfmpt 4056* | Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | nfmpt1 4057 | Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.) |
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | cbvmptf 4058* | 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 4059* | 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 4060* | Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | mptv 4061* | Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.) |
⊢ (𝑥 ∈ V ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ 𝑦 = 𝐵} | ||
Syntax | wtr 4062 | Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35. |
wff Tr 𝐴 | ||
Definition | df-tr 4063 | Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4064 (which is suggestive of the word "transitive"), dftr3 4066, dftr4 4067, and dftr5 4065. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) | ||
Theorem | dftr2 4064* | An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.) |
⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) | ||
Theorem | dftr5 4065* | An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.) |
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴) | ||
Theorem | dftr3 4066* | An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴) | ||
Theorem | dftr4 4067 | An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr 𝐴 ↔ 𝐴 ⊆ 𝒫 𝐴) | ||
Theorem | treq 4068 | Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.) |
⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵)) | ||
Theorem | trel 4069 | 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 4070 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) |
⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐴) → 𝐵 ∈ 𝐴)) | ||
Theorem | trss 4071 | An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.) |
⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) | ||
Theorem | trin 4072 | The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.) |
⊢ ((Tr 𝐴 ∧ Tr 𝐵) → Tr (𝐴 ∩ 𝐵)) | ||
Theorem | tr0 4073 | The empty set is transitive. (Contributed by NM, 16-Sep-1993.) |
⊢ Tr ∅ | ||
Theorem | trv 4074 | The universe is transitive. (Contributed by NM, 14-Sep-2003.) |
⊢ Tr V | ||
Theorem | triun 4075* | The indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | truni 4076* | The union of a class of transitive sets is transitive. Exercise 5(a) of [Enderton] p. 73. (Contributed by Scott Fenton, 21-Feb-2011.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |
⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴) | ||
Theorem | trint 4077* | The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. (Contributed by Scott Fenton, 25-Feb-2011.) |
⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴) | ||
Theorem | trintssm 4078* | Any inhabited transitive class includes its intersection. Similar to Exercise 3 in [TakeutiZaring] p. 44 (which mistakenly does not include the inhabitedness hypothesis). (Contributed by Jim Kingdon, 22-Aug-2018.) |
⊢ ((Tr 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ⊆ 𝐴) | ||
Axiom | ax-coll 4079* | Axiom of Collection. Axiom 7 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). It is similar to bnd 4133 but uses a freeness hypothesis in place of one of the distinct variable conditions. (Contributed by Jim Kingdon, 23-Aug-2018.) |
⊢ Ⅎ𝑏𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑) | ||
Theorem | repizf 4080* | Axiom of Replacement. Axiom 7' of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). In our context this is not an axiom, but a theorem proved from ax-coll 4079. It is identical to zfrep6 4081 except for the choice of a freeness hypothesis rather than a disjoint variable condition between 𝑏 and 𝜑. (Contributed by Jim Kingdon, 23-Aug-2018.) |
⊢ Ⅎ𝑏𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝑎 ∃!𝑦𝜑 → ∃𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑) | ||
Theorem | zfrep6 4081* | A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 4082 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version. (Contributed by NM, 10-Oct-2003.) |
⊢ (∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑) | ||
Axiom | ax-sep 4082* |
The Axiom of Separation of IZF set theory. Axiom 6 of [Crosilla], p.
"Axioms of CZF and IZF" (with unnecessary quantifier removed,
and with a
Ⅎ𝑦𝜑 condition replaced by a disjoint
variable condition between
𝑦 and 𝜑).
The Separation Scheme is a weak form of Frege's Axiom of Comprehension, conditioning it (with 𝑥 ∈ 𝑧) so that it asserts the existence of a collection only if it is smaller than some other collection 𝑧 that already exists. This prevents Russell's paradox ru 2936. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. (Contributed by NM, 11-Sep-2006.) |
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) | ||
Theorem | axsep2 4083* | A less restrictive version of the Separation Scheme ax-sep 4082, where variables 𝑥 and 𝑧 can both appear free in the wff 𝜑, which can therefore be thought of as 𝜑(𝑥, 𝑧). This version was derived from the more restrictive ax-sep 4082 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) | ||
Theorem | zfauscl 4084* | Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 4082, we invoke the Axiom of Extensionality (indirectly via vtocl 2766), which is needed for the justification of class variable notation. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | bm1.3ii 4085* | Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4082. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.) |
⊢ ∃𝑥∀𝑦(𝜑 → 𝑦 ∈ 𝑥) ⇒ ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑) | ||
Theorem | a9evsep 4086* | Derive a weakened version of ax-i9 1510, where 𝑥 and 𝑦 must be distinct, from Separation ax-sep 4082 and Extensionality ax-ext 2139. The theorem ¬ ∀𝑥¬ 𝑥 = 𝑦 also holds (ax9vsep 4087), but in intuitionistic logic ∃𝑥𝑥 = 𝑦 is stronger. (Contributed by Jim Kingdon, 25-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑥 𝑥 = 𝑦 | ||
Theorem | ax9vsep 4087* | Derive a weakened version of ax-9 1511, where 𝑥 and 𝑦 must be distinct, from Separation ax-sep 4082 and Extensionality ax-ext 2139. In intuitionistic logic a9evsep 4086 is stronger and also holds. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | zfnuleu 4088* | Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2142 to strengthen the hypothesis in the form of axnul 4089). (Contributed by NM, 22-Dec-2007.) |
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 ⇒ ⊢ ∃!𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 | ||
Theorem | axnul 4089* |
The Null Set Axiom of ZF set theory: there exists a set with no
elements. Axiom of Empty Set of [Enderton] p. 18. In some textbooks,
this is presented as a separate axiom; here we show it can be derived
from Separation ax-sep 4082. This version of the Null Set Axiom tells us
that at least one empty set exists, but does not tell us that it is
unique - we need the Axiom of Extensionality to do that (see
zfnuleu 4088).
This theorem should not be referenced by any proof. Instead, use ax-nul 4090 below so that the uses of the Null Set Axiom can be more easily identified. (Contributed by Jeff Hoffman, 3-Feb-2008.) (Revised by NM, 4-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 | ||
Axiom | ax-nul 4090* | The Null Set Axiom of IZF set theory. It was derived as axnul 4089 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. Axiom 4 of [Crosilla] p. "Axioms of CZF and IZF". (Contributed by NM, 7-Aug-2003.) |
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 | ||
Theorem | 0ex 4091 | The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 4090. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ ∅ ∈ V | ||
Theorem | csbexga 4092 | The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 𝐵 ∈ 𝑊) → ⦋𝐴 / 𝑥⦌𝐵 ∈ V) | ||
Theorem | csbexa 4093 | The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V | ||
Theorem | nalset 4094* | No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.) |
⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥 | ||
Theorem | vnex 4095 | The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005.) |
⊢ ¬ ∃𝑥 𝑥 = V | ||
Theorem | vprc 4096 | The universal class is not a member of itself (and thus is not a set). Proposition 5.21 of [TakeutiZaring] p. 21; our proof, however, does not depend on the Axiom of Regularity. (Contributed by NM, 23-Aug-1993.) |
⊢ ¬ V ∈ V | ||
Theorem | nvel 4097 | The universal class does not belong to any class. (Contributed by FL, 31-Dec-2006.) |
⊢ ¬ V ∈ 𝐴 | ||
Theorem | inex1 4098 | Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∩ 𝐵) ∈ V | ||
Theorem | inex2 4099 | Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∩ 𝐴) ∈ V | ||
Theorem | inex1g 4100 | Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |