P. 51 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5001-5100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xpidtr 5001	A square cross product (𝐴 × 𝐴) is a transitive relation. (Contributed by FL, 31-Jul-2009.)
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
Theorem	trin2 5002	The intersection of two transitive classes is transitive. (Contributed by FL, 31-Jul-2009.)
⊢ (((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ((𝑅 ∩ 𝑆) ∘ (𝑅 ∩ 𝑆)) ⊆ (𝑅 ∩ 𝑆))
Theorem	poirr2 5003	A partial order relation is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015.)
⊢ (𝑅 Po 𝐴 → (𝑅 ∩ ( I ↾ 𝐴)) = ∅)
Theorem	trinxp 5004	The relation induced by a transitive relation on a part of its field is transitive. (Taking the intersection of a relation with a square cross product is a way to restrict it to a subset of its field.) (Contributed by FL, 31-Jul-2009.)
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴)))
Theorem	soirri 5005	A strict order relation is irreflexive. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ¬ 𝐴𝑅𝐴
Theorem	sotri 5006	A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Theorem	son2lpi 5007	A strict order relation has no 2-cycle loops. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ¬ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴)
Theorem	sotri2 5008	A transitivity relation. (Read ¬ B < A and B < C implies A < C .) (Contributed by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ ¬ 𝐵𝑅𝐴 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Theorem	sotri3 5009	A transitivity relation. (Read A < B and ¬ C < B implies A < C .) (Contributed by Mario Carneiro, 10-May-2013.)
⊢ 𝑅 Or 𝑆    &   ⊢ 𝑅 ⊆ (𝑆 × 𝑆)    ⇒   ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐴𝑅𝐵 ∧ ¬ 𝐶𝑅𝐵) → 𝐴𝑅𝐶)
Theorem	poleloe 5010	Express "less than or equals" for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴(𝑅 ∪ I )𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵)))
Theorem	poltletr 5011	Transitive law for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝑅 Po 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑅𝐵 ∧ 𝐵(𝑅 ∪ I )𝐶) → 𝐴𝑅𝐶))
Theorem	cnvopab 5012*	The converse of a class abstraction of ordered pairs. (Contributed by NM, 11-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ◡{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑦, 𝑥⟩ ∣ 𝜑}
Theorem	mptcnv 5013*	The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐷)))    ⇒   ⊢ (𝜑 → ◡(𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐶 ↦ 𝐷))
Theorem	cnv0 5014	The converse of the empty set. (Contributed by NM, 6-Apr-1998.)
⊢ ◡∅ = ∅
Theorem	cnvi 5015	The converse of the identity relation. Theorem 3.7(ii) of [Monk1] p. 36. (Contributed by NM, 26-Apr-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ◡ I = I
Theorem	cnvun 5016	The converse of a union is the union of converses. Theorem 16 of [Suppes] p. 62. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
Theorem	cnvdif 5017	Distributive law for converse over set difference. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ ◡(𝐴 ∖ 𝐵) = (◡𝐴 ∖ ◡𝐵)
Theorem	cnvin 5018	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 5019	Distributive law for range over union. Theorem 8 of [Suppes] p. 60. (Contributed by NM, 24-Mar-1998.)
⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)
Theorem	rnin 5020	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 5021	The range of an indexed union. (Contributed by Mario Carneiro, 29-May-2015.)
⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵
Theorem	rnuni 5022*	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 5023	Distributive law for image over union. Theorem 35 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.)
⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶))
Theorem	imaundir 5024	The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
⊢ ((𝐴 ∪ 𝐵) “ 𝐶) = ((𝐴 “ 𝐶) ∪ (𝐵 “ 𝐶))
Theorem	dminss 5025	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 5026	An upper bound for intersection with an image. Theorem 41 of [Suppes] p. 66. (Contributed by NM, 11-Aug-2004.)
⊢ ((𝑅 “ 𝐴) ∩ 𝐵) ⊆ (𝑅 “ (𝐴 ∩ (◡𝑅 “ 𝐵)))
Theorem	inimass 5027	The image of an intersection. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ ((𝐴 ∩ 𝐵) “ 𝐶) ⊆ ((𝐴 “ 𝐶) ∩ (𝐵 “ 𝐶))
Theorem	inimasn 5028	The intersection of the image of singleton. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ (𝐶 ∈ 𝑉 → ((𝐴 ∩ 𝐵) “ {𝐶}) = ((𝐴 “ {𝐶}) ∩ (𝐵 “ {𝐶})))
Theorem	cnvxp 5029	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 5030	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 5031*	The cross product of inhabited classes is inhabited. (Contributed by Jim Kingdon, 11-Dec-2018.)
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) ↔ ∃𝑧 𝑧 ∈ (𝐴 × 𝐵))
Theorem	xpm 5032*	The cross product of inhabited classes is inhabited. (Contributed by Jim Kingdon, 13-Dec-2018.)
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) ↔ ∃𝑧 𝑧 ∈ (𝐴 × 𝐵))
Theorem	xpeq0r 5033	A cross product is empty if at least one member is empty. (Contributed by Jim Kingdon, 12-Dec-2018.)
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅)
Theorem	sqxpeq0 5034	A Cartesian square is empty iff its member is empty. (Contributed by Jim Kingdon, 21-Apr-2023.)
⊢ ((𝐴 × 𝐴) = ∅ ↔ 𝐴 = ∅)
Theorem	xpdisj1 5035	Cross products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 × 𝐶) ∩ (𝐵 × 𝐷)) = ∅)
Theorem	xpdisj2 5036	Cross products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 × 𝐴) ∩ (𝐷 × 𝐵)) = ∅)
Theorem	xpsndisj 5037	Cross products with two different singletons are disjoint. (Contributed by NM, 28-Jul-2004.)
⊢ (𝐵 ≠ 𝐷 → ((𝐴 × {𝐵}) ∩ (𝐶 × {𝐷})) = ∅)
Theorem	djudisj 5038*	Disjoint unions with disjoint index sets are disjoint. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐶) ∩ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝐷)) = ∅)
Theorem	resdisj 5039	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 5040*	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 5041	The domain of a cross product is a subclass of the first factor. (Contributed by NM, 19-Mar-2007.)
⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
Theorem	rnxpss 5042	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 5043	Upper bound for the domain of a binary relation. (Contributed by BJ, 10-Jul-2022.)
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → dom 𝑅 ⊆ 𝐴)
Theorem	rnxpss2 5044	Upper bound for the range of a binary relation. (Contributed by BJ, 10-Jul-2022.)
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → ran 𝑅 ⊆ 𝐵)
Theorem	rnxpid 5045	The range of a square cross product. (Contributed by FL, 17-May-2010.)
⊢ ran (𝐴 × 𝐴) = 𝐴
Theorem	ssxpbm 5046*	A cross-product subclass relationship is equivalent to the relationship for its components. (Contributed by Jim Kingdon, 12-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ (𝐴 × 𝐵) → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷)))
Theorem	ssxp1 5047*	Cross product subset cancellation. (Contributed by Jim Kingdon, 14-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) ⊆ (𝐵 × 𝐶) ↔ 𝐴 ⊆ 𝐵))
Theorem	ssxp2 5048*	Cross product subset cancellation. (Contributed by Jim Kingdon, 14-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) ⊆ (𝐶 × 𝐵) ↔ 𝐴 ⊆ 𝐵))
Theorem	xp11m 5049*	The cross product of inhabited classes is one-to-one. (Contributed by Jim Kingdon, 13-Dec-2018.)
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	xpcanm 5050*	Cancellation law for cross-product. (Contributed by Jim Kingdon, 14-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) = (𝐶 × 𝐵) ↔ 𝐴 = 𝐵))
Theorem	xpcan2m 5051*	Cancellation law for cross-product. (Contributed by Jim Kingdon, 14-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) = (𝐵 × 𝐶) ↔ 𝐴 = 𝐵))
Theorem	xpexr2m 5052*	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 5053	Subset of the range of a restriction. (Contributed by NM, 16-Jan-2006.)
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵)
Theorem	rninxp 5054*	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 5055*	Domain of the intersection with a cross product. (Contributed by NM, 17-Jan-2006.)
⊢ (dom (𝐶 ∩ (𝐴 × 𝐵)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥𝐶𝑦)
Theorem	imainrect 5056	Image of a relation restricted to a rectangular region. (Contributed by Stefan O'Rear, 19-Feb-2015.)
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) “ 𝑌) = ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵)
Theorem	xpima1 5057	The image by a cross product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅)
Theorem	xpima2m 5058*	The image by a cross product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ (∃𝑥 𝑥 ∈ (𝐴 ∩ 𝐶) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵)
Theorem	xpimasn 5059	The image of a singleton by a cross product. (Contributed by Thierry Arnoux, 14-Jan-2018.)
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵)
Theorem	cnvcnv3 5060*	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 5061	Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.)
⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)
Theorem	dfrel4v 5062*	A relation can be expressed as the set of ordered pairs in it. (Contributed by Mario Carneiro, 16-Aug-2015.)
⊢ (Rel 𝑅 ↔ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦})
Theorem	cnvcnv 5063	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 5064	The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.)
⊢ ◡◡𝐴 = (𝐴 ↾ V)
Theorem	cnvcnvss 5065	The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 23-Jul-2004.)
⊢ ◡◡𝐴 ⊆ 𝐴
Theorem	cnveqb 5066	Equality theorem for converse. (Contributed by FL, 19-Sep-2011.)
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ◡𝐴 = ◡𝐵))
Theorem	cnveq0 5067	A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.)
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ◡𝐴 = ∅))
Theorem	dfrel3 5068	Alternate definition of relation. (Contributed by NM, 14-May-2008.)
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅)
Theorem	dmresv 5069	The domain of a universal restriction. (Contributed by NM, 14-May-2008.)
⊢ dom (𝐴 ↾ V) = dom 𝐴
Theorem	rnresv 5070	The range of a universal restriction. (Contributed by NM, 14-May-2008.)
⊢ ran (𝐴 ↾ V) = ran 𝐴
Theorem	dfrn4 5071	Range defined in terms of image. (Contributed by NM, 14-May-2008.)
⊢ ran 𝐴 = (𝐴 “ V)
Theorem	csbrng 5072	Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵)
Theorem	rescnvcnv 5073	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 5074	The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007.)
⊢ ◡◡(𝐴 ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵)
Theorem	imacnvcnv 5075	The image of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
⊢ (◡◡𝐴 “ 𝐵) = (𝐴 “ 𝐵)
Theorem	dmsnm 5076*	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 5077*	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 5078	The domain of the singleton of the empty set is empty. (Contributed by NM, 30-Jan-2004.)
⊢ dom {∅} = ∅
Theorem	cnvsn0 5079	The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ◡{∅} = ∅
Theorem	dmsn0el 5080	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 5081*	A singleton is a relation iff it has an inhabited domain. (Contributed by Jim Kingdon, 16-Dec-2018.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Rel {𝐴} ↔ ∃𝑥 𝑥 ∈ dom {𝐴})
Theorem	dmsnopg 5082	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 5083	The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐴, 𝐶})
Theorem	dmsnop 5084	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 5085	The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐴, 𝐶}
Theorem	dmtpop 5086	The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} = {𝐴, 𝐶, 𝐸}
Theorem	cnvcnvsn 5087	Double converse of a singleton of an ordered pair. (Unlike cnvsn 5093, this does not need any sethood assumptions on 𝐴 and 𝐵.) (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ◡◡{⟨𝐴, 𝐵⟩} = ◡{⟨𝐵, 𝐴⟩}
Theorem	dmsnsnsng 5088	The domain of the singleton of the singleton of a singleton. (Contributed by Jim Kingdon, 16-Dec-2018.)
⊢ (𝐴 ∈ V → dom {{{𝐴}}} = {𝐴})
Theorem	rnsnopg 5089	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 5090	The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} = {𝐶, 𝐷})
Theorem	rnsnop 5091	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 5092	Extract the first member of an ordered pair. (See op2nda 5095 to extract the second member and op1stb 4463 for an alternate version.) (Contributed by Raph Levien, 4-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = 𝐴
Theorem	cnvsn 5093	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 5094	Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 4463 to extract the first member and op2nda 5095 for an alternate version.) (Contributed by NM, 25-Nov-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ ∩ ∩ ◡{⟨𝐴, 𝐵⟩} = 𝐵
Theorem	op2nda 5095	Extract the second member of an ordered pair. (See op1sta 5092 to extract the first member and op2ndb 5094 for an alternate version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ ran {⟨𝐴, 𝐵⟩} = 𝐵
Theorem	cnvsng 5096	Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{⟨𝐴, 𝐵⟩} = {⟨𝐵, 𝐴⟩})
Theorem	opswapg 5097	Swap the members of an ordered pair. (Contributed by Jim Kingdon, 16-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ ◡{⟨𝐴, 𝐵⟩} = ⟨𝐵, 𝐴⟩)
Theorem	elxp4 5098	Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp5 5099. (Contributed by NM, 17-Feb-2004.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
Theorem	elxp5 5099	Membership in a cross product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 5098 when the double intersection does not create class existence problems (caused by int0 3845). (Contributed by NM, 1-Aug-2004.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
Theorem	cnvresima 5100	An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.)
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴)