P. 50 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4901-5000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnvdif 4901	Distributive law for converse over set difference. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ ◡(𝐴 ∖ 𝐵) = (◡𝐴 ∖ ◡𝐵)
Theorem	cnvin 4902	Distributive law for converse over intersection. Theorem 15 of [Suppes] p. 62. (Contributed by NM, 25-Mar-1998.) (Revised by Mario Carneiro, 26-Jun-2014.)
⊢ ◡(𝐴 ∩ 𝐵) = (◡𝐴 ∩ ◡𝐵)
Theorem	rnun 4903	Distributive law for range over union. Theorem 8 of [Suppes] p. 60. (Contributed by NM, 24-Mar-1998.)
⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)
Theorem	rnin 4904	The range of an intersection belongs the intersection of ranges. Theorem 9 of [Suppes] p. 60. (Contributed by NM, 15-Sep-2004.)
⊢ ran (𝐴 ∩ 𝐵) ⊆ (ran 𝐴 ∩ ran 𝐵)
Theorem	rniun 4905	The range of an indexed union. (Contributed by Mario Carneiro, 29-May-2015.)
⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵
Theorem	rnuni 4906*	The range of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 17-Mar-2004.) (Revised by Mario Carneiro, 29-May-2015.)
⊢ ran ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ran 𝑥
Theorem	imaundi 4907	Distributive law for image over union. Theorem 35 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.)
⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶))
Theorem	imaundir 4908	The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
⊢ ((𝐴 ∪ 𝐵) “ 𝐶) = ((𝐴 “ 𝐶) ∪ (𝐵 “ 𝐶))
Theorem	dminss 4909	An upper bound for intersection with a domain. Theorem 40 of [Suppes] p. 66, who calls it "somewhat surprising." (Contributed by NM, 11-Aug-2004.)
⊢ (dom 𝑅 ∩ 𝐴) ⊆ (◡𝑅 “ (𝑅 “ 𝐴))
Theorem	imainss 4910	An upper bound for intersection with an image. Theorem 41 of [Suppes] p. 66. (Contributed by NM, 11-Aug-2004.)
⊢ ((𝑅 “ 𝐴) ∩ 𝐵) ⊆ (𝑅 “ (𝐴 ∩ (◡𝑅 “ 𝐵)))
Theorem	inimass 4911	The image of an intersection (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ ((𝐴 ∩ 𝐵) “ 𝐶) ⊆ ((𝐴 “ 𝐶) ∩ (𝐵 “ 𝐶))
Theorem	inimasn 4912	The intersection of the image of singleton (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ (𝐶 ∈ 𝑉 → ((𝐴 ∩ 𝐵) “ {𝐶}) = ((𝐴 “ {𝐶}) ∩ (𝐵 “ {𝐶})))
Theorem	cnvxp 4913	The converse of a cross product. Exercise 11 of [Suppes] p. 67. (Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴)
Theorem	xp0 4914	The cross product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 12-Apr-2004.)
⊢ (𝐴 × ∅) = ∅
Theorem	xpmlem 4915*	The cross product of inhabited classes is inhabited. (Contributed by Jim Kingdon, 11-Dec-2018.)
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) ↔ ∃𝑧 𝑧 ∈ (𝐴 × 𝐵))
Theorem	xpm 4916*	The cross product of inhabited classes is inhabited. (Contributed by Jim Kingdon, 13-Dec-2018.)
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) ↔ ∃𝑧 𝑧 ∈ (𝐴 × 𝐵))
Theorem	xpeq0r 4917	A cross product is empty if at least one member is empty. (Contributed by Jim Kingdon, 12-Dec-2018.)
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅)
Theorem	sqxpeq0 4918	A Cartesian square is empty iff its member is empty. (Contributed by Jim Kingdon, 21-Apr-2023.)
⊢ ((𝐴 × 𝐴) = ∅ ↔ 𝐴 = ∅)
Theorem	xpdisj1 4919	Cross products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 × 𝐶) ∩ (𝐵 × 𝐷)) = ∅)
Theorem	xpdisj2 4920	Cross products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 × 𝐴) ∩ (𝐷 × 𝐵)) = ∅)
Theorem	xpsndisj 4921	Cross products with two different singletons are disjoint. (Contributed by NM, 28-Jul-2004.)
⊢ (𝐵 ≠ 𝐷 → ((𝐴 × {𝐵}) ∩ (𝐶 × {𝐷})) = ∅)
Theorem	djudisj 4922*	Disjoint unions with disjoint index sets are disjoint. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐶) ∩ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝐷)) = ∅)
Theorem	resdisj 4923	A double restriction to disjoint classes is the empty set. (Contributed by NM, 7-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 ↾ 𝐴) ↾ 𝐵) = ∅)
Theorem	rnxpm 4924*	The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37, with nonempty changed to inhabited. (Contributed by Jim Kingdon, 12-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ran (𝐴 × 𝐵) = 𝐵)
Theorem	dmxpss 4925	The domain of a cross product is a subclass of the first factor. (Contributed by NM, 19-Mar-2007.)
⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
Theorem	rnxpss 4926	The range of a cross product is a subclass of the second factor. (Contributed by NM, 16-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
Theorem	dmxpss2 4927	Upper bound for the domain of a binary relation. (Contributed by BJ, 10-Jul-2022.)
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → dom 𝑅 ⊆ 𝐴)
Theorem	rnxpss2 4928	Upper bound for the range of a binary relation. (Contributed by BJ, 10-Jul-2022.)
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → ran 𝑅 ⊆ 𝐵)
Theorem	rnxpid 4929	The range of a square cross product. (Contributed by FL, 17-May-2010.)
⊢ ran (𝐴 × 𝐴) = 𝐴
Theorem	ssxpbm 4930*	A cross-product subclass relationship is equivalent to the relationship for its components. (Contributed by Jim Kingdon, 12-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ (𝐴 × 𝐵) → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷)))
Theorem	ssxp1 4931*	Cross product subset cancellation. (Contributed by Jim Kingdon, 14-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) ⊆ (𝐵 × 𝐶) ↔ 𝐴 ⊆ 𝐵))
Theorem	ssxp2 4932*	Cross product subset cancellation. (Contributed by Jim Kingdon, 14-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) ⊆ (𝐶 × 𝐵) ↔ 𝐴 ⊆ 𝐵))
Theorem	xp11m 4933*	The cross product of inhabited classes is one-to-one. (Contributed by Jim Kingdon, 13-Dec-2018.)
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	xpcanm 4934*	Cancellation law for cross-product. (Contributed by Jim Kingdon, 14-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) = (𝐶 × 𝐵) ↔ 𝐴 = 𝐵))
Theorem	xpcan2m 4935*	Cancellation law for cross-product. (Contributed by Jim Kingdon, 14-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) = (𝐵 × 𝐶) ↔ 𝐴 = 𝐵))
Theorem	xpexr2m 4936*	If a nonempty cross product is a set, so are both of its components. (Contributed by Jim Kingdon, 14-Dec-2018.)
⊢ (((𝐴 × 𝐵) ∈ 𝐶 ∧ ∃𝑥 𝑥 ∈ (𝐴 × 𝐵)) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	ssrnres 4937	Subset of the range of a restriction. (Contributed by NM, 16-Jan-2006.)
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵)
Theorem	rninxp 4938*	Range of the intersection with a cross product. (Contributed by NM, 17-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐶𝑦)
Theorem	dminxp 4939*	Domain of the intersection with a cross product. (Contributed by NM, 17-Jan-2006.)
⊢ (dom (𝐶 ∩ (𝐴 × 𝐵)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥𝐶𝑦)
Theorem	imainrect 4940	Image of a relation restricted to a rectangular region. (Contributed by Stefan O'Rear, 19-Feb-2015.)
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) “ 𝑌) = ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵)
Theorem	xpima1 4941	The image by a cross product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅)
Theorem	xpima2m 4942*	The image by a cross product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ (∃𝑥 𝑥 ∈ (𝐴 ∩ 𝐶) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵)
Theorem	xpimasn 4943	The image of a singleton by a cross product. (Contributed by Thierry Arnoux, 14-Jan-2018.)
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵)
Theorem	cnvcnv3 4944*	The set of all ordered pairs in a class is the same as the double converse. (Contributed by Mario Carneiro, 16-Aug-2015.)
⊢ ◡◡𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦}
Theorem	dfrel2 4945	Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.)
⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)
Theorem	dfrel4v 4946*	A relation can be expressed as the set of ordered pairs in it. (Contributed by Mario Carneiro, 16-Aug-2015.)
⊢ (Rel 𝑅 ↔ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦})
Theorem	cnvcnv 4947	The double converse of a class strips out all elements that are not ordered pairs. (Contributed by NM, 8-Dec-2003.)
⊢ ◡◡𝐴 = (𝐴 ∩ (V × V))
Theorem	cnvcnv2 4948	The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.)
⊢ ◡◡𝐴 = (𝐴 ↾ V)
Theorem	cnvcnvss 4949	The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 23-Jul-2004.)
⊢ ◡◡𝐴 ⊆ 𝐴
Theorem	cnveqb 4950	Equality theorem for converse. (Contributed by FL, 19-Sep-2011.)
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ◡𝐴 = ◡𝐵))
Theorem	cnveq0 4951	A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.)
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ◡𝐴 = ∅))
Theorem	dfrel3 4952	Alternate definition of relation. (Contributed by NM, 14-May-2008.)
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅)
Theorem	dmresv 4953	The domain of a universal restriction. (Contributed by NM, 14-May-2008.)
⊢ dom (𝐴 ↾ V) = dom 𝐴
Theorem	rnresv 4954	The range of a universal restriction. (Contributed by NM, 14-May-2008.)
⊢ ran (𝐴 ↾ V) = ran 𝐴
Theorem	dfrn4 4955	Range defined in terms of image. (Contributed by NM, 14-May-2008.)
⊢ ran 𝐴 = (𝐴 “ V)
Theorem	csbrng 4956	Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵)
Theorem	rescnvcnv 4957	The restriction of the double converse of a class. (Contributed by NM, 8-Apr-2007.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (◡◡𝐴 ↾ 𝐵) = (𝐴 ↾ 𝐵)
Theorem	cnvcnvres 4958	The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007.)
⊢ ◡◡(𝐴 ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵)
Theorem	imacnvcnv 4959	The image of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
⊢ (◡◡𝐴 “ 𝐵) = (𝐴 “ 𝐵)
Theorem	dmsnm 4960*	The domain of a singleton is inhabited iff the singleton argument is an ordered pair. (Contributed by Jim Kingdon, 15-Dec-2018.)
⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥 𝑥 ∈ dom {𝐴})
Theorem	rnsnm 4961*	The range of a singleton is inhabited iff the singleton argument is an ordered pair. (Contributed by Jim Kingdon, 15-Dec-2018.)
⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥 𝑥 ∈ ran {𝐴})
Theorem	dmsn0 4962	The domain of the singleton of the empty set is empty. (Contributed by NM, 30-Jan-2004.)
⊢ dom {∅} = ∅
Theorem	cnvsn0 4963	The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ◡{∅} = ∅
Theorem	dmsn0el 4964	The domain of a singleton is empty if the singleton's argument contains the empty set. (Contributed by NM, 15-Dec-2008.)
⊢ (∅ ∈ 𝐴 → dom {𝐴} = ∅)
Theorem	relsn2m 4965*	A singleton is a relation iff it has an inhabited domain. (Contributed by Jim Kingdon, 16-Dec-2018.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Rel {𝐴} ↔ ∃𝑥 𝑥 ∈ dom {𝐴})
Theorem	dmsnopg 4966	The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐵 ∈ 𝑉 → dom {⟨𝐴, 𝐵⟩} = {𝐴})
Theorem	dmpropg 4967	The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐴, 𝐶})
Theorem	dmsnop 4968	The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐵 ∈ V    ⇒   ⊢ dom {⟨𝐴, 𝐵⟩} = {𝐴}
Theorem	dmprop 4969	The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐴, 𝐶}
Theorem	dmtpop 4970	The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} = {𝐴, 𝐶, 𝐸}
Theorem	cnvcnvsn 4971	Double converse of a singleton of an ordered pair. (Unlike cnvsn 4977, this does not need any sethood assumptions on 𝐴 and 𝐵.) (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ◡◡{⟨𝐴, 𝐵⟩} = ◡{⟨𝐵, 𝐴⟩}
Theorem	dmsnsnsng 4972	The domain of the singleton of the singleton of a singleton. (Contributed by Jim Kingdon, 16-Dec-2018.)
⊢ (𝐴 ∈ V → dom {{{𝐴}}} = {𝐴})
Theorem	rnsnopg 4973	The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → ran {⟨𝐴, 𝐵⟩} = {𝐵})
Theorem	rnpropg 4974	The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} = {𝐶, 𝐷})
Theorem	rnsnop 4975	The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ran {⟨𝐴, 𝐵⟩} = {𝐵}
Theorem	op1sta 4976	Extract the first member of an ordered pair. (See op2nda 4979 to extract the second member and op1stb 4357 for an alternate version.) (Contributed by Raph Levien, 4-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = 𝐴
Theorem	cnvsn 4977	Converse of a singleton of an ordered pair. (Contributed by NM, 11-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ◡{⟨𝐴, 𝐵⟩} = {⟨𝐵, 𝐴⟩}
Theorem	op2ndb 4978	Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 4357 to extract the first member and op2nda 4979 for an alternate version.) (Contributed by NM, 25-Nov-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ ∩ ∩ ◡{⟨𝐴, 𝐵⟩} = 𝐵
Theorem	op2nda 4979	Extract the second member of an ordered pair. (See op1sta 4976 to extract the first member and op2ndb 4978 for an alternate version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ ran {⟨𝐴, 𝐵⟩} = 𝐵
Theorem	cnvsng 4980	Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{⟨𝐴, 𝐵⟩} = {⟨𝐵, 𝐴⟩})
Theorem	opswapg 4981	Swap the members of an ordered pair. (Contributed by Jim Kingdon, 16-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ ◡{⟨𝐴, 𝐵⟩} = ⟨𝐵, 𝐴⟩)
Theorem	elxp4 4982	Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp5 4983. (Contributed by NM, 17-Feb-2004.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
Theorem	elxp5 4983	Membership in a cross product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 4982 when the double intersection does not create class existence problems (caused by int0 3749). (Contributed by NM, 1-Aug-2004.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
Theorem	cnvresima 4984	An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.)
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴)
Theorem	resdm2 4985	A class restricted to its domain equals its double converse. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 ↾ dom 𝐴) = ◡◡𝐴
Theorem	resdmres 4986	Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵)
Theorem	imadmres 4987	The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 “ dom (𝐴 ↾ 𝐵)) = (𝐴 “ 𝐵)
Theorem	mptpreima 4988*	The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
Theorem	mptiniseg 4989*	Converse singleton image of a function defined by maps-to. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝐶 ∈ 𝑉 → (◡𝐹 “ {𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶})
Theorem	dmmpt 4990	The domain of the mapping operation in general. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 22-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
Theorem	dmmptss 4991*	The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ dom 𝐹 ⊆ 𝐴
Theorem	dmmptg 4992*	The domain of the mapping operation is the stated domain, if the function value is always a set. (Contributed by Mario Carneiro, 9-Feb-2013.) (Revised by Mario Carneiro, 14-Sep-2013.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)
Theorem	relco 4993	A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.)
⊢ Rel (𝐴 ∘ 𝐵)
Theorem	dfco2 4994*	Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008.)
⊢ (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))
Theorem	dfco2a 4995*	Generalization of dfco2 4994, where 𝐶 can have any value between dom 𝐴 ∩ ran 𝐵 and V. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ 𝐶 ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})))
Theorem	coundi 4996	Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶))
Theorem	coundir 4997	Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 ∪ 𝐵) ∘ 𝐶) = ((𝐴 ∘ 𝐶) ∪ (𝐵 ∘ 𝐶))
Theorem	cores 4998	Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵))
Theorem	resco 4999	Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.)
⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶))
Theorem	imaco 5000	Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.)
⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶))