![]() |
Metamath
Proof Explorer Theorem List (p. 53 of 486) | < 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-30851) |
![]() (30852-32374) |
![]() (32375-48553) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | brab1 5201* | Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.) |
⊢ (𝑥𝑅𝐴 ↔ 𝑥 ∈ {𝑧 ∣ 𝑧𝑅𝐴}) | ||
Theorem | br0 5202 | The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.) |
⊢ ¬ 𝐴∅𝐵 | ||
Theorem | brne0 5203 | If two sets are in a binary relation, the relation cannot be empty. (Contributed by Alexander van der Vekens, 7-Jul-2018.) |
⊢ (𝐴𝑅𝐵 → 𝑅 ≠ ∅) | ||
Theorem | brun 5204 | The union of two binary relations. (Contributed by NM, 21-Dec-2008.) |
⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵)) | ||
Theorem | brin 5205 | The intersection of two relations. (Contributed by FL, 7-Oct-2008.) |
⊢ (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐵)) | ||
Theorem | brdif 5206 | The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.) |
⊢ (𝐴(𝑅 ∖ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵)) | ||
Theorem | sbcbr123 5207 | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Revised by NM, 22-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝑅⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | sbcbr 5208* | Move substitution in and out of a binary relation. (Contributed by NM, 23-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵⦋𝐴 / 𝑥⦌𝑅𝐶) | ||
Theorem | sbcbr12g 5209* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | sbcbr1g 5210* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵𝑅𝐶)) | ||
Theorem | sbcbr2g 5211* | Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵𝑅𝐶 ↔ 𝐵𝑅⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | brsymdif 5212 | Characterization of the symmetric difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ (𝐴(𝑅 △ 𝑆)𝐵 ↔ ¬ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) | ||
Theorem | brralrspcev 5213* | Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.) |
⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥) | ||
Theorem | brimralrspcev 5214* | 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 5215 | Extend class notation to include ordered-pair class abstraction (class builder). |
class {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Definition | df-opab 5216* | 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 5582 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 8066. An example is given by ex-opab 30365. (Contributed by NM, 4-Jul-1994.) |
⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} | ||
Theorem | opabss 5217* | 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 5218 | 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 5219* | Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) | ||
Theorem | opabbii 5220 | Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} | ||
Theorem | nfopabd 5221* | Bound-variable hypothesis builder for class abstraction. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑧𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑧{〈𝑥, 𝑦〉 ∣ 𝜓}) | ||
Theorem | nfopab 5222* | Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011.) (Revised by Scott Fenton, 26-Oct-2024.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ Ⅎ𝑧{〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | nfopab1 5223 | The first abstraction variable in an ordered-pair class abstraction is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥{〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | nfopab2 5224 | The second abstraction variable in an ordered-pair class abstraction is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑦{〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | cbvopab 5225* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑤〉 ∣ 𝜓} | ||
Theorem | cbvopabv 5226* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.) Reduce axiom usage. (Revised by GG, 15-Oct-2024.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑤〉 ∣ 𝜓} | ||
Theorem | cbvopabvOLD 5227* | Obsolete version of cbvopabv 5226 as of 15-Oct-2024. (Contributed by NM, 15-Oct-1996.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑤〉 ∣ 𝜓} | ||
Theorem | cbvopab1 5228* | 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 2366. See cbvopab1g 5229 for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ 𝜓} | ||
Theorem | cbvopab1g 5229* | 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 2366. See cbvopab1 5228 for a version with more disjoint variable conditions, but not requiring ax-13 2366. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ 𝜓} | ||
Theorem | cbvopab2 5230* | Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑧〉 ∣ 𝜓} | ||
Theorem | cbvopab1s 5231* | Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.) |
⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ [𝑧 / 𝑥]𝜑} | ||
Theorem | cbvopab1v 5232* | 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.) Reduce axiom usage. (Revised by GG, 17-Nov-2024.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ 𝜓} | ||
Theorem | cbvopab1vOLD 5233* | Obsolete version of cbvopab1v 5232 as of 17-Nov-2024. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ 𝜓} | ||
Theorem | cbvopab2v 5234* | Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑧〉 ∣ 𝜓} | ||
Theorem | unopab 5235 | Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∪ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∨ 𝜓)} | ||
Syntax | cmpt 5236 | Extend the definition of a class to include maps-to notation for defining a function via a rule. |
class (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Definition | df-mpt 5237* | 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 | mpteq12da 5238 | An equality inference for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) Remove dependency on ax-10 2130. (Revised by SN, 11-Nov-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12df 5239 | An equality inference for the maps-to notation. Compare mpteq12dv 5244. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) (Proof shortened by SN, 11-Nov-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12dfOLD 5240 | Obsolete version of mpteq12df 5239 as of 11-Nov-2024. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12f 5241 | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12dva 5242* | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) Remove dependency on ax-10 2130, ax-12 2167. (Revised by SN, 11-Nov-2024.) |
⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12dvaOLD 5243* | Obsolete version of mpteq12dva 5242 as of 11-Nov-2024. (Contributed by Mario Carneiro, 26-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12dv 5244* | An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) Remove dependency on ax-10 2130, ax-12 2167. (Revised by SN and GG, 1-Dec-2023.) |
⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq12 5245* | An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.) |
⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | mpteq1 5246* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.) |
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | mpteq1OLD 5247* | Obsolete version of mpteq1 5246 as of 11-Nov-2024. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | mpteq1d 5248* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | mpteq1i 5249 | An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) Remove all disjoint variable conditions. (Revised by SN, 11-Nov-2024.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | mpteq1iOLD 5250* | Obsolete version of mpteq1i 5249 as of 15-Nov-2024. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | mpteq2da 5251 | Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | ||
Theorem | mpteq2daOLD 5252 | Obsolete version of mpteq2da 5251 as of 11-Nov-2024. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | ||
Theorem | mpteq2dva 5253* | Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) Remove dependency on ax-10 2130. (Revised by SN, 11-Nov-2024.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | ||
Theorem | mpteq2dvaOLD 5254* | Obsolete version of mpteq2dva 5253 as of 11-Nov-2024. (Contributed by Scott Fenton, 25-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | ||
Theorem | mpteq2dv 5255* | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | ||
Theorem | mpteq2ia 5256 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.) |
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | mpteq2iaOLD 5257 | Obsolete version of mpteq2ia 5256 as of 11-Nov-2024. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | mpteq2i 5258 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | mpteq12i 5259 | An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.) |
⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷) | ||
Theorem | nfmpt 5260* | Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | nfmpt1 5261 | Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.) |
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | cbvmptf 5262* | 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 2366. See cbvmptfg 5263 for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | cbvmptfg 5263 | 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 2366. See cbvmptf 5262 for a version with more disjoint variable conditions, but not requiring ax-13 2366. (Contributed by NM, 11-Sep-2011.) (Revised by Thierry Arnoux, 9-Mar-2017.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | cbvmpt 5264* | 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 2366. See cbvmptg 5265 for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | cbvmptg 5265* | 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 2366. See cbvmpt 5264 for a version with more disjoint variable conditions, but not requiring ax-13 2366. (Contributed by NM, 11-Sep-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | cbvmptv 5266* | 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 auxiliary axioms . See cbvmptvg 5268 for a less restrictive version requiring more axioms. (Revised by GG, 17-Nov-2024.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | cbvmptvOLD 5267* | Obsolete version of cbvmptv 5266 as of 17-Nov-2024. (Contributed by Mario Carneiro, 19-Feb-2013.) Add disjoint variable condition to avoid ax-13 2366. See cbvmptvg 5268 for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | cbvmptvg 5268* | 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 2366. See cbvmptv 5266 for a version with more disjoint variable conditions, but not requiring ax-13 2366. (Contributed by Mario Carneiro, 19-Feb-2013.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | mptv 5269* | Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.) |
⊢ (𝑥 ∈ V ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ 𝑦 = 𝐵} | ||
Syntax | wtr 5270 | Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35. |
wff Tr 𝐴 | ||
Definition | df-tr 5271 | Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 6122). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 5272 (which is suggestive of the word "transitive"), dftr2c 5273, dftr3 5276, dftr4 5277, dftr5 5274, and (when 𝐴 is a set) unisuc 6455. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) | ||
Theorem | dftr2 5272* | An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. Using dftr2c 5273 instead may avoid dependences on ax-11 2147. (Contributed by NM, 24-Apr-1994.) |
⊢ (Tr 𝐴 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) | ||
Theorem | dftr2c 5273* | Variant of dftr2 5272 with commuted quantifiers, useful for shortening proofs and avoiding ax-11 2147. (Contributed by BTernaryTau, 28-Dec-2024.) |
⊢ (Tr 𝐴 ↔ ∀𝑦∀𝑥((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)) | ||
Theorem | dftr5 5274* | An alternate way of defining a transitive class. Definition 1.1 of [Schloeder] p. 1. (Contributed by NM, 20-Mar-2004.) Avoid ax-11 2147. (Revised by BTernaryTau, 28-Dec-2024.) |
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴) | ||
Theorem | dftr5OLD 5275* | Obsolete version of dftr5 5274 as of 28-Dec-2024. (Contributed by NM, 20-Mar-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐴) | ||
Theorem | dftr3 5276* | An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr 𝐴 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴) | ||
Theorem | dftr4 5277 | An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.) |
⊢ (Tr 𝐴 ↔ 𝐴 ⊆ 𝒫 𝐴) | ||
Theorem | treq 5278 | Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.) |
⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵)) | ||
Theorem | trel 5279 | 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 5280 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) |
⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐴) → 𝐵 ∈ 𝐴)) | ||
Theorem | trss 5281 | 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 5282 | The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.) |
⊢ ((Tr 𝐴 ∧ Tr 𝐵) → Tr (𝐴 ∩ 𝐵)) | ||
Theorem | tr0 5283 | The empty set is transitive. (Contributed by NM, 16-Sep-1993.) |
⊢ Tr ∅ | ||
Theorem | trv 5284 | The universe is transitive. (Contributed by NM, 14-Sep-2003.) |
⊢ Tr V | ||
Theorem | triun 5285 | An indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | truni 5286* | 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 5287 | An indexed intersection of a class of transitive sets is transitive. (Contributed by BJ, 3-Oct-2022.) |
⊢ (∀𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∩ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | trint 5288* | 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 5289 | 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 5290* |
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 6647). 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 5296, where you can
find some further remarks. A slightly more compact version is shown as
axrep2 5293. A quite different variant is zfrep6 7968, which if used in
place of ax-rep 5290 would also require that the Separation Scheme
axsep 5303
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 9934 and the Boundedness Axiom bnd 9935. Many developments of set theory distinguish the uses of Replacement from uses of the weaker axioms of Separation axsep 5303, Null Set axnul 5310, and Pairing axpr 5432, 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 5304, ax-nul 5311, and ax-pr 5433 below the theorems that prove them. (Contributed by NM, 23-Dec-1993.) |
⊢ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))) | ||
Theorem | axrep1 5291* | 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 5290 → axrep1 5291 → axrep2 5293 → axrepnd 10637 → zfcndrep 10657 = ax-rep 5290. (Contributed by NM, 19-Nov-2005.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) Remove dependency on ax-13 2366. (Revised by BJ, 31-May-2019.) |
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ 𝜑))) | ||
Theorem | axreplem 5292* | Lemma for axrep2 5293 and axrep3 5294. (Contributed by BJ, 6-Aug-2022.) |
⊢ (𝑥 = 𝑦 → (∃𝑢(𝜑 → ∀𝑣(𝜓 ↔ ∃𝑤(𝑧 ∈ 𝑥 ∧ 𝜒))) ↔ ∃𝑢(𝜑 → ∀𝑣(𝜓 ↔ ∃𝑤(𝑧 ∈ 𝑦 ∧ 𝜒))))) | ||
Theorem | axrep2 5293* | 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 2366. (Revised by BJ, 31-May-2019.) |
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))) | ||
Theorem | axrep3 5294* | Axiom of Replacement slightly strengthened from axrep2 5293; 𝑤 may occur free in 𝜑. (Contributed by NM, 2-Jan-1997.) Remove dependency on ax-13 2366. (Revised by BJ, 31-May-2019.) |
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑))) | ||
Theorem | axrep4 5295* | A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) | ||
Theorem | axrep5 5296* | 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 5297* | A condensed form of ax-rep 5290. (Contributed by SN, 18-Sep-2023.) |
⊢ (∀𝑤∃*𝑧𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑥 𝜑)) | ||
Theorem | axrep6g 5298* | axrep6 5297 in class notation. It is equivalent to both ax-rep 5290 and abrexexg 7974, providing a direct link between the two. (Contributed by SN, 11-Dec-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥∃*𝑦𝜓) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜓} ∈ V) | ||
Theorem | zfrepclf 5299* | An inference based on the Axiom of Replacement. Typically, 𝜑 defines a function from 𝑥 to 𝑦. (Contributed by NM, 26-Nov-1995.) |
⊢ Ⅎ𝑥𝐴 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧)) ⇒ ⊢ ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | zfrep3cl 5300* | An inference based on the Axiom of Replacement. Typically, 𝜑 defines a function from 𝑥 to 𝑦. (Contributed by NM, 26-Nov-1995.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧)) ⇒ ⊢ ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |