Home | Metamath
Proof Explorer Theorem List (p. 68 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfoprab2 6701* | Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.) |
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)} | ||
Theorem | reloprab 6702* | An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.) |
⊢ Rel {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} | ||
Theorem | oprabv 6703* | If a pair and a class are in a relationship given by a class abstraction of a collection of nested ordered pairs, the involved classes are sets. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
⊢ (〈𝑋, 𝑌〉{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}𝑍 → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)) | ||
Theorem | nfoprab1 6704 | The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ Ⅎ𝑥{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} | ||
Theorem | nfoprab2 6705 | The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 30-Jul-2012.) |
⊢ Ⅎ𝑦{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} | ||
Theorem | nfoprab3 6706 | The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.) |
⊢ Ⅎ𝑧{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} | ||
Theorem | nfoprab 6707* | Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.) |
⊢ Ⅎ𝑤𝜑 ⇒ ⊢ Ⅎ𝑤{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} | ||
Theorem | oprabbid 6708* | Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜒}) | ||
Theorem | oprabbidv 6709* | Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜒}) | ||
Theorem | oprabbii 6710* | Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} | ||
Theorem | ssoprab2 6711 | Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 5001. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓}) | ||
Theorem | ssoprab2b 6712 | Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 5002. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
⊢ ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓)) | ||
Theorem | eqoprab2b 6713 | Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 5005. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓)) | ||
Theorem | mpt2eq123 6714* | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.) |
⊢ ((𝐴 = 𝐷 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐸 ∧ ∀𝑦 ∈ 𝐵 𝐶 = 𝐹)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) | ||
Theorem | mpt2eq12 6715* | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) | ||
Theorem | mpt2eq123dva 6716* | An equality deduction for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) | ||
Theorem | mpt2eq123dv 6717* | An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.) |
⊢ (𝜑 → 𝐴 = 𝐷) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) | ||
Theorem | mpt2eq123i 6718 | An equality inference for the maps to notation. (Contributed by NM, 15-Jul-2013.) |
⊢ 𝐴 = 𝐷 & ⊢ 𝐵 = 𝐸 & ⊢ 𝐶 = 𝐹 ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹) | ||
Theorem | mpt2eq3dva 6719* | Slightly more general equality inference for the maps to notation. (Contributed by NM, 17-Oct-2013.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) | ||
Theorem | mpt2eq3ia 6720 | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | mpt2eq3dv 6721* | An equality deduction for the maps to notation restricted to the value of the operation. (Contributed by SO, 16-Jul-2018.) |
⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) | ||
Theorem | nfmpt21 6722 | Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.) |
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | nfmpt22 6723 | Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.) |
⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | nfmpt2 6724* | Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |
⊢ Ⅎ𝑧𝐴 & ⊢ Ⅎ𝑧𝐵 & ⊢ Ⅎ𝑧𝐶 ⇒ ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | mpt20 6725 | A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅ | ||
Theorem | oprab4 6726* | Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.) |
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} | ||
Theorem | cbvoprab1 6727* | Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008.) (Revised by Mario Carneiro, 5-Dec-2016.) |
⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑤, 𝑦〉, 𝑧〉 ∣ 𝜓} | ||
Theorem | cbvoprab2 6728* | Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑤 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑥, 𝑤〉, 𝑧〉 ∣ 𝜓} | ||
Theorem | cbvoprab12 6729* | Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑣𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑣) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑤, 𝑣〉, 𝑧〉 ∣ 𝜓} | ||
Theorem | cbvoprab12v 6730* | Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.) |
⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑣) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑤, 𝑣〉, 𝑧〉 ∣ 𝜓} | ||
Theorem | cbvoprab3 6731* | Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.) |
⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑧𝜓 & ⊢ (𝑧 = 𝑤 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑥, 𝑦〉, 𝑤〉 ∣ 𝜓} | ||
Theorem | cbvoprab3v 6732* | Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ (𝑧 = 𝑤 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑥, 𝑦〉, 𝑤〉 ∣ 𝜓} | ||
Theorem | cbvmpt2x 6733* | Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 6734 allows 𝐵 to be a function of 𝑥. (Contributed by NM, 29-Dec-2014.) |
⊢ Ⅎ𝑧𝐵 & ⊢ Ⅎ𝑥𝐷 & ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑤𝐶 & ⊢ Ⅎ𝑥𝐸 & ⊢ Ⅎ𝑦𝐸 & ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐷) & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐸) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐷 ↦ 𝐸) | ||
Theorem | cbvmpt2 6734* | Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.) |
⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑤𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ Ⅎ𝑦𝐷 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | cbvmpt2v 6735* | Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 4749, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.) |
⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸) & ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | elimdelov 6736 | Eliminate a hypothesis which is a predicate expressing membership in the result of an operator (deduction version). (Contributed by Paul Chapman, 25-Mar-2008.) |
⊢ (𝜑 → 𝐶 ∈ (𝐴𝐹𝐵)) & ⊢ 𝑍 ∈ (𝑋𝐹𝑌) ⇒ ⊢ if(𝜑, 𝐶, 𝑍) ∈ (if(𝜑, 𝐴, 𝑋)𝐹if(𝜑, 𝐵, 𝑌)) | ||
Theorem | ovif 6737 | Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (if(𝜑, 𝐴, 𝐵)𝐹𝐶) = if(𝜑, (𝐴𝐹𝐶), (𝐵𝐹𝐶)) | ||
Theorem | ovif2 6738 | Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 1-Oct-2018.) |
⊢ (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = if(𝜑, (𝐴𝐹𝐵), (𝐴𝐹𝐶)) | ||
Theorem | ovif12 6739 | Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (if(𝜑, 𝐴, 𝐵)𝐹if(𝜑, 𝐶, 𝐷)) = if(𝜑, (𝐴𝐹𝐶), (𝐵𝐹𝐷)) | ||
Theorem | ifov 6740 | Move a conditional outside of an operation. (Contributed by AV, 11-Nov-2019.) |
⊢ (𝐴if(𝜑, 𝐹, 𝐺)𝐵) = if(𝜑, (𝐴𝐹𝐵), (𝐴𝐺𝐵)) | ||
Theorem | dmoprab 6741* | The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ ∃𝑧𝜑} | ||
Theorem | dmoprabss 6742* | The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995.) |
⊢ dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) | ||
Theorem | rnoprab 6743* | The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.) |
⊢ ran {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦𝜑} | ||
Theorem | rnoprab2 6744* | The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.) |
⊢ ran {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} | ||
Theorem | reldmoprab 6745* | The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.) |
⊢ Rel dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} | ||
Theorem | oprabss 6746* | Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.) |
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ ((V × V) × V) | ||
Theorem | eloprabga 6747* | The law of concretion for operation class abstraction. Compare elopab 4983. (Contributed by NM, 14-Sep-1999.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | eloprabg 6748* | The law of concretion for operation class abstraction. Compare elopab 4983. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜃)) | ||
Theorem | ssoprab2i 6749* | Inference of operation class abstraction subclass from implication. (Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} | ||
Theorem | mpt2v 6750* | Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.) |
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝐶} | ||
Theorem | mpt2mptx 6751* | Express a two-argument function as a one-argument function, or vice-versa. In this version 𝐵(𝑥) is not assumed to be constant w.r.t 𝑥. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | mpt2mpt 6752* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | mpt2difsnif 6753 | A mapping with two arguments with the first argument from a difference set with a singleton and a conditional as result. (Contributed by AV, 13-Feb-2019.) |
⊢ (𝑖 ∈ (𝐴 ∖ {𝑋}), 𝑗 ∈ 𝐵 ↦ if(𝑖 = 𝑋, 𝐶, 𝐷)) = (𝑖 ∈ (𝐴 ∖ {𝑋}), 𝑗 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | mpt2snif 6754 | A mapping with two arguments with the first argument from a singleton and a conditional as result. (Contributed by AV, 14-Feb-2019.) |
⊢ (𝑖 ∈ {𝑋}, 𝑗 ∈ 𝐵 ↦ if(𝑖 = 𝑋, 𝐶, 𝐷)) = (𝑖 ∈ {𝑋}, 𝑗 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | fconstmpt2 6755* | Representation of a constant operation using the mapping operation. (Contributed by SO, 11-Jul-2018.) |
⊢ ((𝐴 × 𝐵) × {𝐶}) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | resoprab 6756* | Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007.) |
⊢ ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↾ (𝐴 × 𝐵)) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} | ||
Theorem | resoprab2 6757* | Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ↾ (𝐶 × 𝐷)) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)}) | ||
Theorem | resmpt2 6758* | Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.) |
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) ↾ (𝐶 × 𝐷)) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) | ||
Theorem | funoprabg 6759* | "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 28-Aug-2007.) |
⊢ (∀𝑥∀𝑦∃*𝑧𝜑 → Fun {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}) | ||
Theorem | funoprab 6760* | "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 17-Mar-1995.) |
⊢ ∃*𝑧𝜑 ⇒ ⊢ Fun {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} | ||
Theorem | fnoprabg 6761* | Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007.) |
⊢ (∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)} Fn {〈𝑥, 𝑦〉 ∣ 𝜑}) | ||
Theorem | mpt2fun 6762* | The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ Fun 𝐹 | ||
Theorem | fnoprab 6763* | Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995.) |
⊢ (𝜑 → ∃!𝑧𝜓) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)} Fn {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | ffnov 6764* | An operation maps to a class to which all values belong. (Contributed by NM, 7-Feb-2004.) |
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶)) | ||
Theorem | fovcl 6765 | Closure law for an operation. (Contributed by NM, 19-Apr-2007.) |
⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶 ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) | ||
Theorem | eqfnov 6766* | Equality of two operations is determined by their values. (Contributed by NM, 1-Sep-2005.) |
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐶 × 𝐷)) → (𝐹 = 𝐺 ↔ ((𝐴 × 𝐵) = (𝐶 × 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦)))) | ||
Theorem | eqfnov2 6767* | Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010.) |
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐴 × 𝐵)) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦))) | ||
Theorem | fnov 6768* | Representation of a function in terms of its values. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐹 Fn (𝐴 × 𝐵) ↔ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝑥𝐹𝑦))) | ||
Theorem | mpt22eqb 6769* | Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 6767. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 = 𝐷)) | ||
Theorem | rnmpt2 6770* | The range of an operation given by the "maps to" notation. (Contributed by FL, 20-Jun-2011.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} | ||
Theorem | reldmmpt2 6771* | The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ Rel dom 𝐹 | ||
Theorem | elrnmpt2g 6772* | Membership in the range of an operation class abstraction. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝐷 ∈ 𝑉 → (𝐷 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶)) | ||
Theorem | elrnmpt2 6773* | Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐷 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶) | ||
Theorem | elrnmpt2res 6774* | Membership in the range of a restricted operation class abstraction. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝐷 ∈ 𝑉 → (𝐷 ∈ ran (𝐹 ↾ 𝑅) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐷 = 𝐶 ∧ 𝑥𝑅𝑦))) | ||
Theorem | ralrnmpt2 6775* | A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ (𝑧 = 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → (∀𝑧 ∈ ran 𝐹𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | rexrnmpt2 6776* | A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ (𝑧 = 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → (∃𝑧 ∈ ran 𝐹𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | ovid 6777* | The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃!𝑧𝜑) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = 𝑧 ↔ 𝜑)) | ||
Theorem | ovidig 6778* | The value of an operation class abstraction. Compare ovidi 6779. The condition (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ ∃*𝑧𝜑 & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⇒ ⊢ (𝜑 → (𝑥𝐹𝑦) = 𝑧) | ||
Theorem | ovidi 6779* | The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃*𝑧𝜑) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → (𝜑 → (𝑥𝐹𝑦) = 𝑧)) | ||
Theorem | ov 6780* | The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ 𝐶 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃!𝑧𝜑) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵) = 𝐶 ↔ 𝜃)) | ||
Theorem | ovigg 6781* | The value of an operation class abstraction. Compare ovig 6782. The condition (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) is been removed. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ ∃*𝑧𝜑 & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝜓 → (𝐴𝐹𝐵) = 𝐶)) | ||
Theorem | ovig 6782* | The value of an operation class abstraction (weak version). (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 14-Sep-1999.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃*𝑧𝜑) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷) → (𝜓 → (𝐴𝐹𝐵) = 𝐶)) | ||
Theorem | ovmpt4g 6783* | Value of a function given by the "maps to" notation. (This is the operation analogue of fvmpt2 6291.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) = 𝐶) | ||
Theorem | ovmpt2s 6784* | Value of a function given by the "maps to" notation, expressed using explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝑅 ∈ 𝑉) → (𝐴𝐹𝐵) = ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝑅) | ||
Theorem | ov2gf 6785* | The value of an operation class abstraction. A version of ovmpt2g 6795 using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐺 & ⊢ Ⅎ𝑦𝑆 & ⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺) & ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpt2dxf 6786* | Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐿) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑆 & ⊢ Ⅎ𝑦𝑆 ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpt2dx 6787* | Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐿) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpt2d 6788* | Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpt2x 6789* | The value of an operation class abstraction. Variant of ovmpt2ga 6790 which does not require 𝐷 and 𝑥 to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) & ⊢ (𝑥 = 𝐴 → 𝐷 = 𝐿) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpt2ga 6790* | Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpt2a 6791* | Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) & ⊢ 𝑆 ∈ V ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpt2df 6792* | Alternate deduction version of ovmpt2 6796, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅 → 𝜓)) & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝐹 & ⊢ Ⅎ𝑦𝜓 ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) | ||
Theorem | ovmpt2dv 6793* | Alternate deduction version of ovmpt2 6796, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅 → 𝜓)) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) | ||
Theorem | ovmpt2dv2 6794* | Alternate deduction version of ovmpt2 6796, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → (𝐴𝐹𝐵) = 𝑆)) | ||
Theorem | ovmpt2g 6795* | Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺) & ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpt2 6796* | Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺) & ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) & ⊢ 𝑆 ∈ V ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ov3 6797* | The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 ∈ V & ⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 𝑅 = 𝑆) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))} ⇒ ⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑆) | ||
Theorem | ov6g 6798* | The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006.) |
⊢ (〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 → 𝑅 = 𝑆) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (〈𝑥, 𝑦〉 ∈ 𝐶 ∧ 𝑧 = 𝑅)} ⇒ ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ 〈𝐴, 𝐵〉 ∈ 𝐶) ∧ 𝑆 ∈ 𝐽) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovg 6799* | The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝜏 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)) → ∃!𝑧𝜑) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → ((𝐴𝐹𝐵) = 𝐶 ↔ 𝜃)) | ||
Theorem | ovres 6800 | The value of a restricted operation. (Contributed by FL, 10-Nov-2006.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |