Home | Metamath
Proof Explorer Theorem List (p. 52 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eqbrtrid 5101 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrrid 5102 | A chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrid 5103 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrrid 5104 | A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
⊢ 𝐴𝑅𝐵 & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrdi 5105 | A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrrdi 5106 | A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrdi 5107 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrrdi 5108 | A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | ssbrd 5109 | Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) | ||
Theorem | ssbr 5110 | Implication from a subclass relationship of binary relations. (Contributed by Peter Mazsa, 11-Nov-2019.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) | ||
Theorem | ssbri 5111 | Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷) | ||
Theorem | nfbrd 5112 | Deduction version of bound-variable hypothesis builder nfbr 5113. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝑅) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴𝑅𝐵) | ||
Theorem | nfbr 5113 | Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴𝑅𝐵 | ||
Theorem | brab1 5114* | Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.) |
⊢ (𝑥𝑅𝐴 ↔ 𝑥 ∈ {𝑧 ∣ 𝑧𝑅𝐴}) | ||
Theorem | br0 5115 | The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.) |
⊢ ¬ 𝐴∅𝐵 | ||
Theorem | brne0 5116 | If two sets are in a binary relation, the relation cannot be empty. (Contributed by Alexander van der Vekens, 7-Jul-2018.) |
⊢ (𝐴𝑅𝐵 → 𝑅 ≠ ∅) | ||
Theorem | brun 5117 | The union of two binary relations. (Contributed by NM, 21-Dec-2008.) |
⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵)) | ||
Theorem | brin 5118 | The intersection of two relations. (Contributed by FL, 7-Oct-2008.) |
⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵)) | ||
Theorem | brdif 5119 | The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.) |
⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵)) | ||
Theorem | sbcbr123 5120 | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Revised by NM, 22-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝑅⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | sbcbr 5121* | Move substitution in and out of a binary relation. (Contributed by NM, 23-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵⦋𝐴 / 𝑥⦌𝑅𝐶) | ||
Theorem | sbcbr12g 5122* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | sbcbr1g 5123* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅𝐶)) | ||
Theorem | sbcbr2g 5124* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵𝑅⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | brsymdif 5125 | Characterization of the symmetric difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ (𝐴(𝑅 △ 𝑆)𝐵 ↔ ¬ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) | ||
Theorem | brralrspcev 5126* | Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.) |
⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥) | ||
Theorem | brimralrspcev 5127* | 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 5128 | Extend class notation to include ordered-pair class abstraction (class builder). |
class {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Definition | df-opab 5129* | Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually 𝑥 and 𝑦 are distinct, although the definition does not require it (see dfid2 5463 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also called "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 7750. An example is given by ex-opab 28211. (Contributed by NM, 4-Jul-1994.) |
⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} | ||
Theorem | opabss 5130* | 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 5131 | 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 5132* | Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) | ||
Theorem | opabbii 5133 | Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} | ||
Theorem | nfopab 5134* | 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 5135 | 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 5136 | 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 5137* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑤〉 ∣ 𝜓} | ||
Theorem | cbvopabv 5138* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑤〉 ∣ 𝜓} | ||
Theorem | cbvopab1 5139* | 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.) Add disjoint variable condition to avoid ax-13 2390. See cbvopab1g 5140 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ 𝜓} | ||
Theorem | cbvopab1g 5140* | Change first bound variable in an ordered-pair class abstraction, using explicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. See cbvopab1 5139 for a version with more disjoint variable conditions, but not requiring ax-13 2390. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ 𝜓} | ||
Theorem | cbvopab2 5141* | Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑧〉 ∣ 𝜓} | ||
Theorem | cbvopab1s 5142* | Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.) |
⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ [𝑧 / 𝑥]𝜑} | ||
Theorem | cbvopab1v 5143* | 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 5144* | Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑧〉 ∣ 𝜓} | ||
Theorem | unopab 5145 | Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∪ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∨ 𝜓)} | ||
Syntax | cmpt 5146 | Extend the definition of a class to include maps-to notation for defining a function via a rule. |
class (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Definition | df-mpt 5147* | 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 | mpteq12df 5148 | An equality inference for the maps-to notation. Compare mpteq12dv 5151. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12f 5149 | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12dva 5150* | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12dv 5151* | An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) Drop ax-10 2145 while shortening its proof. (Revised by Steven Nguyen and Gino Giotto, 1-Dec-2023.) |
⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12dvOLD 5152* | Obsolete version of mpteq12dv 5151 as of 1-Dec-2023. (Contributed by NM, 24-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12 5153* | An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.) |
⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq1 5154* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | mpteq1d 5155* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | mpteq1i 5156* | An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | mpteq2ia 5157 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | mpteq2i 5158 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | mpteq12i 5159 | An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.) |
⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷) | ||
Theorem | mpteq2da 5160 | 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 5161* | Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | ||
Theorem | mpteq2dv 5162* | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | ||
Theorem | nfmpt 5163* | Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | nfmpt1 5164 | Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.) |
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | cbvmptf 5165* | 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.) (Revised by Thierry Arnoux, 9-Mar-2017.) Add disjoint variable condition to avoid ax-13 2390. See cbvmptfg 5166 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | cbvmptfg 5166 | 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. Usage of this theorem is discouraged because it depends on ax-13 2390. See cbvmptf 5165 for a version with more disjoint variable conditions, but not requiring ax-13 2390. (Contributed by NM, 11-Sep-2011.) (Revised by Thierry Arnoux, 9-Mar-2017.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | cbvmpt 5167* | 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.) Add disjoint variable condition to avoid ax-13 2390. See cbvmptg 5168 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | cbvmptg 5168* | 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. Usage of this theorem is discouraged because it depends on ax-13 2390. See cbvmpt 5167 for a version with more disjoint variable conditions, but not requiring ax-13 2390. (Contributed by NM, 11-Sep-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | cbvmptv 5169* | Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) Add disjoint variable condition to avoid ax-13 2390. See cbvmptvg 5170 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | cbvmptvg 5170* | Rule to change the bound variable in a maps-to function, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. See cbvmptv 5169 for a version with more disjoint variable conditions, but not requiring ax-13 2390. (Contributed by Mario Carneiro, 19-Feb-2013.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | mptv 5171* | Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.) |
⊢ (𝑥 ∈ V ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ 𝑦 = 𝐵} | ||
Syntax | wtr 5172 | Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35. |
wff Tr 𝐴 | ||
Definition | df-tr 5173 | Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 5972). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 5174 (which is suggestive of the word "transitive"), dftr3 5176, dftr4 5177, dftr5 5175, and (when 𝐴 is a set) unisuc 6267. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) | ||
Theorem | dftr2 5174* | An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.) |
⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) | ||
Theorem | dftr5 5175* | An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.) |
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴) | ||
Theorem | dftr3 5176* | An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴) | ||
Theorem | dftr4 5177 | An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr 𝐴 ↔ 𝐴 ⊆ 𝒫 𝐴) | ||
Theorem | treq 5178 | Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.) |
⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵)) | ||
Theorem | trel 5179 | 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 5180 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) |
⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐴) → 𝐵 ∈ 𝐴)) | ||
Theorem | trss 5181 | 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 5182 | The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.) |
⊢ ((Tr 𝐴 ∧ Tr 𝐵) → Tr (𝐴 ∩ 𝐵)) | ||
Theorem | tr0 5183 | The empty set is transitive. (Contributed by NM, 16-Sep-1993.) |
⊢ Tr ∅ | ||
Theorem | trv 5184 | The universe is transitive. (Contributed by NM, 14-Sep-2003.) |
⊢ Tr V | ||
Theorem | triun 5185 | An indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | truni 5186* | 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 | triin 5187 | An indexed intersection of a class of transitive sets is transitive. (Contributed by BJ, 3-Oct-2022.) |
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∩ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | trint 5188* | The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by BJ, 3-Oct-2022.) |
⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴) | ||
Theorem | trintss 5189 | Any nonempty transitive class includes its intersection. Exercise 3 in [TakeutiZaring] p. 44 (which mistakenly does not include the nonemptiness hypothesis). (Contributed by Scott Fenton, 3-Mar-2011.) (Proof shortened by Andrew Salmon, 14-Nov-2011.) |
⊢ ((Tr 𝐴 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ⊆ 𝐴) | ||
Axiom | ax-rep 5190* |
Axiom of Replacement. An axiom scheme of Zermelo-Fraenkel set theory.
Axiom 5 of [TakeutiZaring] p. 19.
It tells us that the image of any set
under a function is also a set (see the variant funimaex 6441). Although
𝜑 may be any wff whatsoever, this
axiom is useful (i.e. its
antecedent is satisfied) when we are given some function and 𝜑
encodes the predicate "the value of the function at 𝑤 is
𝑧".
Thus, 𝜑 will ordinarily have free variables
𝑤
and 𝑧- think
of it informally as 𝜑(𝑤, 𝑧). We prefix 𝜑 with the
quantifier ∀𝑦 in order to "protect" the
axiom from any 𝜑
containing 𝑦, thus allowing us to eliminate any
restrictions on
𝜑. Another common variant is derived
as axrep5 5196, where you can
find some further remarks. A slightly more compact version is shown as
axrep2 5193. A quite different variant is zfrep6 7656, which if used in
place of ax-rep 5190 would also require that the Separation Scheme
axsep 5202
be stated as a separate axiom.
There is a very strong generalization of Replacement that doesn't demand function-like behavior of 𝜑. Two versions of this generalization are called the Collection Principle cp 9320 and the Boundedness Axiom bnd 9321. Many developments of set theory distinguish the uses of Replacement from uses of the weaker axioms of Separation axsep 5202, Null Set axnul 5209, and Pairing axpr 5329, all of which we derive from Replacement. In order to make it easier to identify the uses of those redundant axioms, we restate them as axioms ax-sep 5203, ax-nul 5210, and ax-pr 5330 below the theorems that prove them. (Contributed by NM, 23-Dec-1993.) |
⊢ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))) | ||
Theorem | axrep1 5191* | The version of the Axiom of Replacement used in the Metamath Solitaire applet https://us.metamath.org/mmsolitaire/mms.html. Equivalence is shown via the path ax-rep 5190 → axrep1 5191 → axrep2 5193 → axrepnd 10016 → zfcndrep 10036 = ax-rep 5190. (Contributed by NM, 19-Nov-2005.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) Remove dependency on ax-13 2390. (Revised by BJ, 31-May-2019.) |
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ 𝜑))) | ||
Theorem | axreplem 5192* | Lemma for axrep2 5193 and axrep3 5194. (Contributed by BJ, 6-Aug-2022.) |
⊢ (𝑥 = 𝑦 → (∃𝑢(𝜑 → ∀𝑣(𝜓 ↔ ∃𝑤(𝑧 ∈ 𝑥 ∧ 𝜒))) ↔ ∃𝑢(𝜑 → ∀𝑣(𝜓 ↔ ∃𝑤(𝑧 ∈ 𝑦 ∧ 𝜒))))) | ||
Theorem | axrep2 5193* | Axiom of Replacement expressed with the fewest number of different variables and without any restrictions on 𝜑. (Contributed by NM, 15-Aug-2003.) Remove dependency on ax-13 2390. (Revised by BJ, 31-May-2019.) |
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))) | ||
Theorem | axrep3 5194* | Axiom of Replacement slightly strengthened from axrep2 5193; 𝑤 may occur free in 𝜑. (Contributed by NM, 2-Jan-1997.) Remove dependency on ax-13 2390. (Revised by BJ, 31-May-2019.) |
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑))) | ||
Theorem | axrep4 5195* | A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) | ||
Theorem | axrep5 5196* | Axiom of Replacement (similar to Axiom Rep of [BellMachover] p. 463). The antecedent tells us 𝜑 is analogous to a "function" from 𝑥 to 𝑦 (although it is not really a function since it is a wff and not a class). In the consequent we postulate the existence of a set 𝑧 that corresponds to the "image" of 𝜑 restricted to some other set 𝑤. The hypothesis says 𝑧 must not be free in 𝜑. (Contributed by NM, 26-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (∀𝑥(𝑥 ∈ 𝑤 → ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧)) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) | ||
Theorem | axrep6 5197* | A condensed form of ax-rep 5190. (Contributed by SN, 18-Sep-2023.) |
⊢ (∀𝑤∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑)) | ||
Theorem | zfrepclf 5198* | An inference based on the Axiom of Replacement. Typically, 𝜑 defines a function from 𝑥 to 𝑦. (Contributed by NM, 26-Nov-1995.) |
⊢ Ⅎ𝑥𝐴 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧)) ⇒ ⊢ ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | zfrep3cl 5199* | An inference based on the Axiom of Replacement. Typically, 𝜑 defines a function from 𝑥 to 𝑦. (Contributed by NM, 26-Nov-1995.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧)) ⇒ ⊢ ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | zfrep4 5200* | A version of Replacement using class abstractions. (Contributed by NM, 26-Nov-1995.) |
⊢ {𝑥 ∣ 𝜑} ∈ V & ⊢ (𝜑 → ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧)) ⇒ ⊢ {𝑦 ∣ ∃𝑥(𝜑 ∧ 𝜓)} ∈ V |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |