Theorem List for Intuitionistic Logic Explorer - 4801-4900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | rnex 4801 |
The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26.
Similar to Lemma 3D of [Enderton] p.
41. (Contributed by NM,
7-Jul-2008.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ran 𝐴 ∈ V |
|
Theorem | iprc 4802 |
The identity function is a proper class. This means, for example, that we
cannot use it as a member of the class of continuous functions unless it
is restricted to a set. (Contributed by NM, 1-Jan-2007.)
|
⊢ ¬ I ∈ V |
|
Theorem | dmcoss 4803 |
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 4804 |
Range of a composition. (Contributed by NM, 19-Mar-1998.)
|
⊢ ran (𝐴 ∘ 𝐵) ⊆ ran 𝐴 |
|
Theorem | dmcosseq 4805 |
Domain of a composition. (Contributed by NM, 28-May-1998.) (Proof
shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ (ran 𝐵 ⊆ dom 𝐴 → dom (𝐴 ∘ 𝐵) = dom 𝐵) |
|
Theorem | dmcoeq 4806 |
Domain of a composition. (Contributed by NM, 19-Mar-1998.)
|
⊢ (dom 𝐴 = ran 𝐵 → dom (𝐴 ∘ 𝐵) = dom 𝐵) |
|
Theorem | rncoeq 4807 |
Range of a composition. (Contributed by NM, 19-Mar-1998.)
|
⊢ (dom 𝐴 = ran 𝐵 → ran (𝐴 ∘ 𝐵) = ran 𝐴) |
|
Theorem | reseq1 4808 |
Equality theorem for restrictions. (Contributed by NM, 7-Aug-1994.)
|
⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) |
|
Theorem | reseq2 4809 |
Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.)
|
⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) |
|
Theorem | reseq1i 4810 |
Equality inference for restrictions. (Contributed by NM,
21-Oct-2014.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶) |
|
Theorem | reseq2i 4811 |
Equality inference for restrictions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵) |
|
Theorem | reseq12i 4812 |
Equality inference for restrictions. (Contributed by NM,
21-Oct-2014.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷) |
|
Theorem | reseq1d 4813 |
Equality deduction for restrictions. (Contributed by NM,
21-Oct-2014.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) |
|
Theorem | reseq2d 4814 |
Equality deduction for restrictions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) |
|
Theorem | reseq12d 4815 |
Equality deduction for restrictions. (Contributed by NM,
21-Oct-2014.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷)) |
|
Theorem | nfres 4816 |
Bound-variable hypothesis builder for restriction. (Contributed by NM,
15-Sep-2003.) (Revised by David Abernethy, 19-Jun-2012.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵) |
|
Theorem | csbresg 4817 |
Distribute proper substitution through the restriction of a class.
(Contributed by Alan Sare, 10-Nov-2012.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | res0 4818 |
A restriction to the empty set is empty. (Contributed by NM,
12-Nov-1994.)
|
⊢ (𝐴 ↾ ∅) =
∅ |
|
Theorem | opelres 4819 |
Ordered pair membership in a restriction. Exercise 13 of
[TakeutiZaring] p. 25.
(Contributed by NM, 13-Nov-1995.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 ↾ 𝐷) ↔ (〈𝐴, 𝐵〉 ∈ 𝐶 ∧ 𝐴 ∈ 𝐷)) |
|
Theorem | brres 4820 |
Binary relation on a restriction. (Contributed by NM, 12-Dec-2006.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴(𝐶 ↾ 𝐷)𝐵 ↔ (𝐴𝐶𝐵 ∧ 𝐴 ∈ 𝐷)) |
|
Theorem | opelresg 4821 |
Ordered pair membership in a restriction. Exercise 13 of
[TakeutiZaring] p. 25.
(Contributed by NM, 14-Oct-2005.)
|
⊢ (𝐵 ∈ 𝑉 → (〈𝐴, 𝐵〉 ∈ (𝐶 ↾ 𝐷) ↔ (〈𝐴, 𝐵〉 ∈ 𝐶 ∧ 𝐴 ∈ 𝐷))) |
|
Theorem | brresg 4822 |
Binary relation on a restriction. (Contributed by Mario Carneiro,
4-Nov-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴(𝐶 ↾ 𝐷)𝐵 ↔ (𝐴𝐶𝐵 ∧ 𝐴 ∈ 𝐷))) |
|
Theorem | opres 4823 |
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 4824 |
A restricted identity relation is equivalent to equality in its domain.
(Contributed by NM, 30-Apr-2004.)
|
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵( I ↾ 𝐴)𝐶 ↔ 𝐵 = 𝐶)) |
|
Theorem | opelresi 4825 |
〈𝐴,
𝐴〉 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 4826 |
The restriction of a restriction. (Contributed by NM, 27-Mar-2008.)
|
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ (𝐵 ∩ 𝐶)) |
|
Theorem | resundi 4827 |
Distributive law for restriction over union. Theorem 31 of [Suppes]
p. 65. (Contributed by NM, 30-Sep-2002.)
|
⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) |
|
Theorem | resundir 4828 |
Distributive law for restriction over union. (Contributed by NM,
23-Sep-2004.)
|
⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) |
|
Theorem | resindi 4829 |
Class restriction distributes over intersection. (Contributed by FL,
6-Oct-2008.)
|
⊢ (𝐴 ↾ (𝐵 ∩ 𝐶)) = ((𝐴 ↾ 𝐵) ∩ (𝐴 ↾ 𝐶)) |
|
Theorem | resindir 4830 |
Class restriction distributes over intersection. (Contributed by NM,
18-Dec-2008.)
|
⊢ ((𝐴 ∩ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∩ (𝐵 ↾ 𝐶)) |
|
Theorem | inres 4831 |
Move intersection into class restriction. (Contributed by NM,
18-Dec-2008.)
|
⊢ (𝐴 ∩ (𝐵 ↾ 𝐶)) = ((𝐴 ∩ 𝐵) ↾ 𝐶) |
|
Theorem | resdifcom 4832 |
Commutative law for restriction and difference. (Contributed by AV,
7-Jun-2021.)
|
⊢ ((𝐴 ↾ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ↾ 𝐵) |
|
Theorem | resiun1 4833* |
Distribution of restriction over indexed union. (Contributed by Mario
Carneiro, 29-May-2015.)
|
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ↾ 𝐶) = ∪
𝑥 ∈ 𝐴 (𝐵 ↾ 𝐶) |
|
Theorem | resiun2 4834* |
Distribution of restriction over indexed union. (Contributed by Mario
Carneiro, 29-May-2015.)
|
⊢ (𝐶 ↾ ∪ 𝑥 ∈ 𝐴 𝐵) = ∪
𝑥 ∈ 𝐴 (𝐶 ↾ 𝐵) |
|
Theorem | dmres 4835 |
The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25.
(Contributed by NM, 1-Aug-1994.)
|
⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴) |
|
Theorem | ssdmres 4836 |
A domain restricted to a subclass equals the subclass. (Contributed by
NM, 2-Mar-1997.)
|
⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴) |
|
Theorem | dmresexg 4837 |
The domain of a restriction to a set exists. (Contributed by NM,
7-Apr-1995.)
|
⊢ (𝐵 ∈ 𝑉 → dom (𝐴 ↾ 𝐵) ∈ V) |
|
Theorem | resss 4838 |
A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25.
(Contributed by NM, 2-Aug-1994.)
|
⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 |
|
Theorem | rescom 4839 |
Commutative law for restriction. (Contributed by NM, 27-Mar-1998.)
|
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ↾ 𝐵) |
|
Theorem | ssres 4840 |
Subclass theorem for restriction. (Contributed by NM, 16-Aug-1994.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ↾ 𝐶) ⊆ (𝐵 ↾ 𝐶)) |
|
Theorem | ssres2 4841 |
Subclass theorem for restriction. (Contributed by NM, 22-Mar-1998.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵)) |
|
Theorem | relres 4842 |
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 4843 |
Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25.
(Contributed by NM, 9-Aug-1994.)
|
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵)) |
|
Theorem | resabs1d 4844 |
Absorption law for restriction, deduction form. (Contributed by Glauco
Siliprandi, 11-Dec-2019.)
|
⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵)) |
|
Theorem | resabs2 4845 |
Absorption law for restriction. (Contributed by NM, 27-Mar-1998.)
|
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵)) |
|
Theorem | residm 4846 |
Idempotent law for restriction. (Contributed by NM, 27-Mar-1998.)
|
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐵) = (𝐴 ↾ 𝐵) |
|
Theorem | resima 4847 |
A restriction to an image. (Contributed by NM, 29-Sep-2004.)
|
⊢ ((𝐴 ↾ 𝐵) “ 𝐵) = (𝐴 “ 𝐵) |
|
Theorem | resima2 4848 |
Image under a restricted class. (Contributed by FL, 31-Aug-2009.)
|
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) “ 𝐵) = (𝐴 “ 𝐵)) |
|
Theorem | xpssres 4849 |
Restriction of a constant function (or other cross product). (Contributed
by Stefan O'Rear, 24-Jan-2015.)
|
⊢ (𝐶 ⊆ 𝐴 → ((𝐴 × 𝐵) ↾ 𝐶) = (𝐶 × 𝐵)) |
|
Theorem | elres 4850* |
Membership in a restriction. (Contributed by Scott Fenton,
17-Mar-2011.)
|
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵)) |
|
Theorem | elsnres 4851* |
Memebership in restriction to a singleton. (Contributed by Scott
Fenton, 17-Mar-2011.)
|
⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐵 ↾ {𝐶}) ↔ ∃𝑦(𝐴 = 〈𝐶, 𝑦〉 ∧ 〈𝐶, 𝑦〉 ∈ 𝐵)) |
|
Theorem | relssres 4852 |
Simplification law for restriction. (Contributed by NM,
16-Aug-1994.)
|
⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → (𝐴 ↾ 𝐵) = 𝐴) |
|
Theorem | resdm 4853 |
A relation restricted to its domain equals itself. (Contributed by NM,
12-Dec-2006.)
|
⊢ (Rel 𝐴 → (𝐴 ↾ dom 𝐴) = 𝐴) |
|
Theorem | resexg 4854 |
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 4855 |
The restriction of a set is a set. (Contributed by Jeff Madsen,
19-Jun-2011.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ↾ 𝐵) ∈ V |
|
Theorem | resindm 4856 |
When restricting a relation, intersecting with the domain of the relation
has no effect. (Contributed by FL, 6-Oct-2008.)
|
⊢ (Rel 𝐴 → (𝐴 ↾ (𝐵 ∩ dom 𝐴)) = (𝐴 ↾ 𝐵)) |
|
Theorem | resdmdfsn 4857 |
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 4858* |
Restriction of a class abstraction of ordered pairs. (Contributed by
NM, 5-Nov-2002.)
|
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ↾ 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
|
Theorem | resiexg 4859 |
The existence of a restricted identity function, proved without using
the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.)
|
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V) |
|
Theorem | iss 4860 |
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 4861* |
Restriction of a class abstraction of ordered pairs. (Contributed by
NM, 24-Aug-2007.)
|
⊢ (𝐴 ⊆ 𝐵 → ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↾ 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}) |
|
Theorem | resmpt 4862* |
Restriction of the mapping operation. (Contributed by Mario Carneiro,
15-Jul-2013.)
|
⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
|
Theorem | resmpt3 4863* |
Unconditional restriction of the mapping operation. (Contributed by
Stefan O'Rear, 24-Jan-2015.) (Proof shortened by Mario Carneiro,
22-Mar-2015.)
|
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ (𝐴 ∩ 𝐵) ↦ 𝐶) |
|
Theorem | resmptf 4864 |
Restriction of the mapping operation. (Contributed by Thierry Arnoux,
28-Mar-2017.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
|
Theorem | resmptd 4865* |
Restriction of the mapping operation, deduction form. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
|
Theorem | dfres2 4866* |
Alternate definition of the restriction operation. (Contributed by
Mario Carneiro, 5-Nov-2013.)
|
⊢ (𝑅 ↾ 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥𝑅𝑦)} |
|
Theorem | opabresid 4867* |
The restricted identity expressed with the class builder. (Contributed
by FL, 25-Apr-2012.)
|
⊢ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)} = ( I ↾ 𝐴) |
|
Theorem | mptresid 4868* |
The restricted identity expressed with the maps-to notation.
(Contributed by FL, 25-Apr-2012.)
|
⊢ (𝑥 ∈ 𝐴 ↦ 𝑥) = ( I ↾ 𝐴) |
|
Theorem | dmresi 4869 |
The domain of a restricted identity function. (Contributed by NM,
27-Aug-2004.)
|
⊢ dom ( I ↾ 𝐴) = 𝐴 |
|
Theorem | resid 4870 |
Any relation restricted to the universe is itself. (Contributed by NM,
16-Mar-2004.)
|
⊢ (Rel 𝐴 → (𝐴 ↾ V) = 𝐴) |
|
Theorem | imaeq1 4871 |
Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
|
⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) |
|
Theorem | imaeq2 4872 |
Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
|
⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵)) |
|
Theorem | imaeq1i 4873 |
Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶) |
|
Theorem | imaeq2i 4874 |
Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵) |
|
Theorem | imaeq1d 4875 |
Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) |
|
Theorem | imaeq2d 4876 |
Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵)) |
|
Theorem | imaeq12d 4877 |
Equality theorem for image. (Contributed by Mario Carneiro,
4-Dec-2016.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐷)) |
|
Theorem | dfima2 4878* |
Alternate definition of image. Compare definition (d) of [Enderton]
p. 44. (Contributed by NM, 19-Apr-2004.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑥𝐴𝑦} |
|
Theorem | dfima3 4879* |
Alternate definition of image. Compare definition (d) of [Enderton]
p. 44. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ 𝐴)} |
|
Theorem | elimag 4880* |
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 20-Jan-2007.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴)) |
|
Theorem | elima 4881* |
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 19-Apr-2004.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴) |
|
Theorem | elima2 4882* |
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 11-Aug-2004.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝐴)) |
|
Theorem | elima3 4883* |
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 14-Aug-1994.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ 〈𝑥, 𝐴〉 ∈ 𝐵)) |
|
Theorem | nfima 4884 |
Bound-variable hypothesis builder for image. (Contributed by NM,
30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 “ 𝐵) |
|
Theorem | nfimad 4885 |
Deduction version of bound-variable hypothesis builder nfima 4884.
(Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro,
15-Oct-2016.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝐴 “ 𝐵)) |
|
Theorem | imadmrn 4886 |
The image of the domain of a class is the range of the class.
(Contributed by NM, 14-Aug-1994.)
|
⊢ (𝐴 “ dom 𝐴) = ran 𝐴 |
|
Theorem | imassrn 4887 |
The image of a class is a subset of its range. Theorem 3.16(xi) of
[Monk1] p. 39. (Contributed by NM,
31-Mar-1995.)
|
⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴 |
|
Theorem | imaexg 4888 |
The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed
by NM, 24-Jul-1995.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V) |
|
Theorem | imaex 4889 |
The image of a set is a set. Theorem 3.17 of [Monk1] p. 39.
(Contributed by JJ, 24-Sep-2021.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 “ 𝐵) ∈ V |
|
Theorem | imai 4890 |
Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38.
(Contributed by NM, 30-Apr-1998.)
|
⊢ ( I “ 𝐴) = 𝐴 |
|
Theorem | rnresi 4891 |
The range of the restricted identity function. (Contributed by NM,
27-Aug-2004.)
|
⊢ ran ( I ↾ 𝐴) = 𝐴 |
|
Theorem | resiima 4892 |
The image of a restriction of the identity function. (Contributed by FL,
31-Dec-2006.)
|
⊢ (𝐵 ⊆ 𝐴 → (( I ↾ 𝐴) “ 𝐵) = 𝐵) |
|
Theorem | ima0 4893 |
Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed
by NM, 20-May-1998.)
|
⊢ (𝐴 “ ∅) =
∅ |
|
Theorem | 0ima 4894 |
Image under the empty relation. (Contributed by FL, 11-Jan-2007.)
|
⊢ (∅ “ 𝐴) = ∅ |
|
Theorem | csbima12g 4895 |
Move class substitution in and out of the image of a function.
(Contributed by FL, 15-Dec-2006.) (Proof shortened by Mario Carneiro,
4-Dec-2016.)
|
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵)) |
|
Theorem | imadisj 4896 |
A class whose image under another is empty is disjoint with the other's
domain. (Contributed by FL, 24-Jan-2007.)
|
⊢ ((𝐴 “ 𝐵) = ∅ ↔ (dom 𝐴 ∩ 𝐵) = ∅) |
|
Theorem | cnvimass 4897 |
A preimage under any class is included in the domain of the class.
(Contributed by FL, 29-Jan-2007.)
|
⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴 |
|
Theorem | cnvimarndm 4898 |
The preimage of the range of a class is the domain of the class.
(Contributed by Jeff Hankins, 15-Jul-2009.)
|
⊢ (◡𝐴 “ ran 𝐴) = dom 𝐴 |
|
Theorem | imasng 4899* |
The image of a singleton. (Contributed by NM, 8-May-2005.)
|
⊢ (𝐴 ∈ 𝐵 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦}) |
|
Theorem | elreimasng 4900 |
Elementhood in the image of a singleton. (Contributed by Jim Kingdon,
10-Dec-2018.)
|
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑉) → (𝐵 ∈ (𝑅 “ {𝐴}) ↔ 𝐴𝑅𝐵)) |