Home | Metamath
Proof Explorer Theorem List (p. 59 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rneqi 5801 | Equality inference for range. (Contributed by NM, 4-Mar-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ran 𝐴 = ran 𝐵 | ||
Theorem | rneqd 5802 | Equality deduction for range. (Contributed by NM, 4-Mar-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ran 𝐴 = ran 𝐵) | ||
Theorem | rnss 5803 | Subset theorem for range. (Contributed by NM, 22-Mar-1998.) |
⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵) | ||
Theorem | rnssi 5804 | Subclass inference for range. (Contributed by Peter Mazsa, 24-Sep-2022.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ran 𝐴 ⊆ ran 𝐵 | ||
Theorem | brelrng 5805 | The second argument of a binary relation belongs to its range. (Contributed by NM, 29-Jun-2008.) |
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐴𝐶𝐵) → 𝐵 ∈ ran 𝐶) | ||
Theorem | brelrn 5806 | The second argument of a binary relation belongs to its range. (Contributed by NM, 13-Aug-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴𝐶𝐵 → 𝐵 ∈ ran 𝐶) | ||
Theorem | opelrn 5807 | Membership of second member of an ordered pair in a range. (Contributed by NM, 23-Feb-1997.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ 𝐶 → 𝐵 ∈ ran 𝐶) | ||
Theorem | releldm 5808 | The first argument of a binary relation belongs to its domain. Note that 𝐴𝑅𝐵 does not imply Rel 𝑅: see for example nrelv 5667 and brv 5356. (Contributed by NM, 2-Jul-2008.) |
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) | ||
Theorem | relelrn 5809 | The second argument of a binary relation belongs to its range. (Contributed by NM, 2-Jul-2008.) |
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ ran 𝑅) | ||
Theorem | releldmb 5810* | Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.) |
⊢ (Rel 𝑅 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥)) | ||
Theorem | relelrnb 5811* | Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.) |
⊢ (Rel 𝑅 → (𝐴 ∈ ran 𝑅 ↔ ∃𝑥 𝑥𝑅𝐴)) | ||
Theorem | releldmi 5812 | The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.) |
⊢ Rel 𝑅 ⇒ ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) | ||
Theorem | relelrni 5813 | The second argument of a binary relation belongs to its range. (Contributed by NM, 28-Apr-2015.) |
⊢ Rel 𝑅 ⇒ ⊢ (𝐴𝑅𝐵 → 𝐵 ∈ ran 𝑅) | ||
Theorem | dfrnf 5814* | Definition of range, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Aug-1995.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 ⇒ ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} | ||
Theorem | elrn2 5815* | Membership in a range. (Contributed by NM, 10-Jul-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥〈𝑥, 𝐴〉 ∈ 𝐵) | ||
Theorem | elrn 5816* | Membership in a range. (Contributed by NM, 2-Apr-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴) | ||
Theorem | nfdm 5817 | Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥dom 𝐴 | ||
Theorem | nfrn 5818 | Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥ran 𝐴 | ||
Theorem | dmiin 5819 | Domain of an intersection. (Contributed by FL, 15-Oct-2012.) |
⊢ dom ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 dom 𝐵 | ||
Theorem | rnopab 5820* | The range of a class of ordered pairs. (Contributed by NM, 14-Aug-1995.) (Revised by Mario Carneiro, 4-Dec-2016.) |
⊢ ran {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑦 ∣ ∃𝑥𝜑} | ||
Theorem | rnmpt 5821* | The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} | ||
Theorem | elrnmpt 5822* | The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) | ||
Theorem | elrnmpt1s 5823* | Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶) ⇒ ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹) | ||
Theorem | elrnmpt1 5824 | Elementhood in an image set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ ran 𝐹) | ||
Theorem | elrnmptg 5825* | Membership in the range of a function. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) | ||
Theorem | elrnmpti 5826* | Membership in the range of a function. (Contributed by NM, 30-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵) | ||
Theorem | elrnmptdv 5827* | Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐷 ∈ ran 𝐹) | ||
Theorem | elrnmpt2d 5828* | Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ran 𝐹) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝐶 = 𝐵) | ||
Theorem | dfiun3g 5829 | Alternate definition of indexed union when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) | ||
Theorem | dfiin3g 5830 | Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) | ||
Theorem | dfiun3 5831 | Alternate definition of indexed union when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐵 ∈ V ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | dfiin3 5832 | Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐵 ∈ V ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | riinint 5833* | Express a relative indexed intersection as an intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋) → (𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆) = ∩ ({𝑋} ∪ ran (𝑘 ∈ 𝐼 ↦ 𝑆))) | ||
Theorem | relrn0 5834 | A relation is empty iff its range is empty. (Contributed by NM, 15-Sep-2004.) |
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ran 𝐴 = ∅)) | ||
Theorem | dmrnssfld 5835 | The domain and range of a class are included in its double union. (Contributed by NM, 13-May-2008.) |
⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴 | ||
Theorem | dmcoss 5836 | Domain of a composition. Theorem 21 of [Suppes] p. 63. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ dom (𝐴 ∘ 𝐵) ⊆ dom 𝐵 | ||
Theorem | rncoss 5837 | Range of a composition. (Contributed by NM, 19-Mar-1998.) |
⊢ ran (𝐴 ∘ 𝐵) ⊆ ran 𝐴 | ||
Theorem | dmcosseq 5838 | Domain of a composition. (Contributed by NM, 28-May-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (ran 𝐵 ⊆ dom 𝐴 → dom (𝐴 ∘ 𝐵) = dom 𝐵) | ||
Theorem | dmcoeq 5839 | Domain of a composition. (Contributed by NM, 19-Mar-1998.) |
⊢ (dom 𝐴 = ran 𝐵 → dom (𝐴 ∘ 𝐵) = dom 𝐵) | ||
Theorem | rncoeq 5840 | Range of a composition. (Contributed by NM, 19-Mar-1998.) |
⊢ (dom 𝐴 = ran 𝐵 → ran (𝐴 ∘ 𝐵) = ran 𝐴) | ||
Theorem | reseq1 5841 | Equality theorem for restrictions. (Contributed by NM, 7-Aug-1994.) |
⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) | ||
Theorem | reseq2 5842 | Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.) |
⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) | ||
Theorem | reseq1i 5843 | Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶) | ||
Theorem | reseq2i 5844 | Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵) | ||
Theorem | reseq12i 5845 | Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷) | ||
Theorem | reseq1d 5846 | Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) | ||
Theorem | reseq2d 5847 | Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) | ||
Theorem | reseq12d 5848 | Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷)) | ||
Theorem | nfres 5849 | Bound-variable hypothesis builder for restriction. (Contributed by NM, 15-Sep-2003.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵) | ||
Theorem | csbres 5850 | Distribute proper substitution through the restriction of a class. (Contributed by Alan Sare, 10-Nov-2012.) (Revised by NM, 23-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | res0 5851 | A restriction to the empty set is empty. (Contributed by NM, 12-Nov-1994.) |
⊢ (𝐴 ↾ ∅) = ∅ | ||
Theorem | dfres3 5852 | Alternate definition of restriction. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × ran 𝐴)) | ||
Theorem | opelres 5853 | Ordered pair elementhood in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 13-Nov-1995.) (Revised by BJ, 18-Feb-2022.) Commute the consequent. (Revised by Peter Mazsa, 24-Sep-2022.) |
⊢ (𝐶 ∈ 𝑉 → (〈𝐵, 𝐶〉 ∈ (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 〈𝐵, 𝐶〉 ∈ 𝑅))) | ||
Theorem | brres 5854 | Binary relation on a restriction. (Contributed by Mario Carneiro, 4-Nov-2015.) Commute the consequent. (Revised by Peter Mazsa, 24-Sep-2022.) |
⊢ (𝐶 ∈ 𝑉 → (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))) | ||
Theorem | opelresi 5855 | Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 13-Nov-1995.) |
⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐵, 𝐶〉 ∈ (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 〈𝐵, 𝐶〉 ∈ 𝑅)) | ||
Theorem | brresi 5856 | Binary relation on a restriction. (Contributed by NM, 12-Dec-2006.) |
⊢ 𝐶 ∈ V ⇒ ⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)) | ||
Theorem | opres 5857 | Ordered pair membership in a restriction when the first member belongs to the restricting class. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐷 → (〈𝐴, 𝐵〉 ∈ (𝐶 ↾ 𝐷) ↔ 〈𝐴, 𝐵〉 ∈ 𝐶)) | ||
Theorem | resieq 5858 | A restricted identity relation is equivalent to equality in its domain. (Contributed by NM, 30-Apr-2004.) |
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵( I ↾ 𝐴)𝐶 ↔ 𝐵 = 𝐶)) | ||
Theorem | opelidres 5859 | 〈𝐴, 𝐴〉 belongs to a restriction of the identity class iff 𝐴 belongs to the restricting class. (Contributed by FL, 27-Oct-2008.) (Revised by NM, 30-Mar-2016.) |
⊢ (𝐴 ∈ 𝑉 → (〈𝐴, 𝐴〉 ∈ ( I ↾ 𝐵) ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | resres 5860 | The restriction of a restriction. (Contributed by NM, 27-Mar-2008.) |
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ (𝐵 ∩ 𝐶)) | ||
Theorem | resundi 5861 | Distributive law for restriction over union. Theorem 31 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.) |
⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) | ||
Theorem | resundir 5862 | Distributive law for restriction over union. (Contributed by NM, 23-Sep-2004.) |
⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) | ||
Theorem | resindi 5863 | Class restriction distributes over intersection. (Contributed by FL, 6-Oct-2008.) |
⊢ (𝐴 ↾ (𝐵 ∩ 𝐶)) = ((𝐴 ↾ 𝐵) ∩ (𝐴 ↾ 𝐶)) | ||
Theorem | resindir 5864 | Class restriction distributes over intersection. (Contributed by NM, 18-Dec-2008.) |
⊢ ((𝐴 ∩ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∩ (𝐵 ↾ 𝐶)) | ||
Theorem | inres 5865 | Move intersection into class restriction. (Contributed by NM, 18-Dec-2008.) |
⊢ (𝐴 ∩ (𝐵 ↾ 𝐶)) = ((𝐴 ∩ 𝐵) ↾ 𝐶) | ||
Theorem | resdifcom 5866 | Commutative law for restriction and difference. (Contributed by AV, 7-Jun-2021.) |
⊢ ((𝐴 ↾ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ↾ 𝐵) | ||
Theorem | resiun1 5867* | Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015.) (Proof shortened by JJ, 25-Aug-2021.) |
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ↾ 𝐶) = ∪ 𝑥 ∈ 𝐴 (𝐵 ↾ 𝐶) | ||
Theorem | resiun2 5868* | Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015.) |
⊢ (𝐶 ↾ ∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 (𝐶 ↾ 𝐵) | ||
Theorem | dmres 5869 | The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by NM, 1-Aug-1994.) |
⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴) | ||
Theorem | ssdmres 5870 | A domain restricted to a subclass equals the subclass. (Contributed by NM, 2-Mar-1997.) |
⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴) | ||
Theorem | dmresexg 5871 | The domain of a restriction to a set exists. (Contributed by NM, 7-Apr-1995.) |
⊢ (𝐵 ∈ 𝑉 → dom (𝐴 ↾ 𝐵) ∈ V) | ||
Theorem | resss 5872 | A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) |
⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 | ||
Theorem | rescom 5873 | Commutative law for restriction. (Contributed by NM, 27-Mar-1998.) |
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ↾ 𝐵) | ||
Theorem | ssres 5874 | Subclass theorem for restriction. (Contributed by NM, 16-Aug-1994.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ↾ 𝐶) ⊆ (𝐵 ↾ 𝐶)) | ||
Theorem | ssres2 5875 | Subclass theorem for restriction. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵)) | ||
Theorem | relres 5876 | A restriction is a relation. Exercise 12 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ Rel (𝐴 ↾ 𝐵) | ||
Theorem | resabs1 5877 | Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25. (Contributed by NM, 9-Aug-1994.) |
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵)) | ||
Theorem | resabs1d 5878 | Absorption law for restriction, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵)) | ||
Theorem | resabs2 5879 | Absorption law for restriction. (Contributed by NM, 27-Mar-1998.) |
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵)) | ||
Theorem | residm 5880 | Idempotent law for restriction. (Contributed by NM, 27-Mar-1998.) |
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐵) = (𝐴 ↾ 𝐵) | ||
Theorem | resima 5881 | A restriction to an image. (Contributed by NM, 29-Sep-2004.) |
⊢ ((𝐴 ↾ 𝐵) “ 𝐵) = (𝐴 “ 𝐵) | ||
Theorem | resima2 5882 | Image under a restricted class. (Contributed by FL, 31-Aug-2009.) (Proof shortened by JJ, 25-Aug-2021.) |
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) “ 𝐵) = (𝐴 “ 𝐵)) | ||
Theorem | xpssres 5883 | Restriction of a constant function (or other Cartesian product). (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝐶 ⊆ 𝐴 → ((𝐴 × 𝐵) ↾ 𝐶) = (𝐶 × 𝐵)) | ||
Theorem | elinxp 5884* | Membership in an intersection with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022.) |
⊢ (𝐶 ∈ (𝑅 ∩ (𝐴 × 𝐵)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐶 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝑅)) | ||
Theorem | elres 5885* | Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011.) (Proof shortened by Peter Mazsa, 9-Sep-2022.) |
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵)) | ||
Theorem | elsnres 5886* | Membership in restriction to a singleton. (Contributed by Scott Fenton, 17-Mar-2011.) |
⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐵 ↾ {𝐶}) ↔ ∃𝑦(𝐴 = 〈𝐶, 𝑦〉 ∧ 〈𝐶, 𝑦〉 ∈ 𝐵)) | ||
Theorem | relssres 5887 | Simplification law for restriction. (Contributed by NM, 16-Aug-1994.) |
⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → (𝐴 ↾ 𝐵) = 𝐴) | ||
Theorem | dmressnsn 5888 | The domain of a restriction to a singleton is a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ (𝐴 ∈ dom 𝐹 → dom (𝐹 ↾ {𝐴}) = {𝐴}) | ||
Theorem | eldmressnsn 5889 | The element of the domain of a restriction to a singleton is the element of the singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ (𝐴 ∈ dom 𝐹 → 𝐴 ∈ dom (𝐹 ↾ {𝐴})) | ||
Theorem | eldmeldmressn 5890 | An element of the domain (of a relation) is an element of the domain of the restriction (of the relation) to the singleton containing this element. (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
⊢ (𝑋 ∈ dom 𝐹 ↔ 𝑋 ∈ dom (𝐹 ↾ {𝑋})) | ||
Theorem | resdm 5891 | A relation restricted to its domain equals itself. (Contributed by NM, 12-Dec-2006.) |
⊢ (Rel 𝐴 → (𝐴 ↾ dom 𝐴) = 𝐴) | ||
Theorem | resexg 5892 | The restriction of a set is a set. (Contributed by NM, 28-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V) | ||
Theorem | resex 5893 | The restriction of a set is a set. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ↾ 𝐵) ∈ V | ||
Theorem | resindm 5894 | When restricting a relation, intersecting with the domain of the relation has no effect. (Contributed by FL, 6-Oct-2008.) |
⊢ (Rel 𝐴 → (𝐴 ↾ (𝐵 ∩ dom 𝐴)) = (𝐴 ↾ 𝐵)) | ||
Theorem | resdmdfsn 5895 | Restricting a relation to its domain without a set is the same as restricting the relation to the universe without this set. (Contributed by AV, 2-Dec-2018.) |
⊢ (Rel 𝑅 → (𝑅 ↾ (V ∖ {𝑋})) = (𝑅 ↾ (dom 𝑅 ∖ {𝑋}))) | ||
Theorem | resopab 5896* | Restriction of a class abstraction of ordered pairs. (Contributed by NM, 5-Nov-2002.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ↾ 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | ||
Theorem | iss 5897 | A subclass of the identity function is the identity function restricted to its domain. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ⊆ I ↔ 𝐴 = ( I ↾ dom 𝐴)) | ||
Theorem | resopab2 5898* | Restriction of a class abstraction of ordered pairs. (Contributed by NM, 24-Aug-2007.) |
⊢ (𝐴 ⊆ 𝐵 → ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↾ 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}) | ||
Theorem | resmpt 5899* | Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.) |
⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | resmpt3 5900* | Unconditional restriction of the mapping operation. (Contributed by Stefan O'Rear, 24-Jan-2015.) (Proof shortened by Mario Carneiro, 22-Mar-2015.) |
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ (𝐴 ∩ 𝐵) ↦ 𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |