P. 81 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8001-8100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oprabrexex2 8001*	Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.)
⊢ 𝐴 ∈ V    &   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ∈ V    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑤 ∈ 𝐴 𝜑} ∈ V
Theorem	ab2rexex 8002*	Existence of a class abstraction of existentially restricted sets. Variables 𝑥 and 𝑦 are normally free-variable parameters in the class expression substituted for 𝐶, which can be thought of as 𝐶(𝑥, 𝑦). See comments for abrexex 7985. (Contributed by NM, 20-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} ∈ V
Theorem	ab2rexex2 8003*	Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥, 𝑦, and 𝑧. Compare abrexex2 7992. (Contributed by NM, 20-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ {𝑧 ∣ 𝜑} ∈ V    ⇒   ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} ∈ V
Theorem	xpexgALT 8004	Alternate proof of xpexg 7768 requiring Replacement (ax-rep 5284) but not Power Set (ax-pow 5370). (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
Theorem	offval3 8005*	General value of (𝐹 ∘f 𝑅𝐺) with no assumptions on functionality of 𝐹 and 𝐺. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))))
Theorem	offres 8006	Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘f 𝑅𝐺) ↾ 𝐷) = ((𝐹 ↾ 𝐷) ∘f 𝑅(𝐺 ↾ 𝐷)))
Theorem	ofmres 8007*	Equivalent expressions for a restriction of the function operation map. Unlike ∘f 𝑅 which is a proper class, ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) can be a set by ofmresex 8008, allowing it to be used as a function or structure argument. By ofmresval 7712, the restricted operation map values are the same as the original values, allowing theorems for ∘f 𝑅 to be reused. (Contributed by NM, 20-Oct-2014.)
⊢ ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) = (𝑓 ∈ 𝐴, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘f 𝑅𝑔))
Theorem	ofmresex 8008	Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ( ∘f 𝑅 ↾ (𝐴 × 𝐵)) ∈ V)
Theorem	mptcnfimad 8009*	The converse of a mapping of subsets to their image of a bijection. (Contributed by AV, 23-Apr-2025.)
⊢ 𝑀 = (𝑥 ∈ 𝐴 ↦ (𝐹 “ 𝑥))    &   ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝒫 𝑉)    &   ⊢ (𝜑 → ran 𝑀 ⊆ 𝒫 𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ◡𝑀 = (𝑦 ∈ ran 𝑀 ↦ (◡𝐹 “ 𝑦)))
2.4.8  First and second members of an ordered pair
Syntax	c1st 8010	Extend the definition of a class to include the first member an ordered pair function.
class 1st
Syntax	c2nd 8011	Extend the definition of a class to include the second member an ordered pair function.
class 2nd
Definition	df-1st 8012	Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 8020 proves that it does this. For example, (1st ‘⟨3, 4⟩) = 3. Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 6246 and op1stb 5481). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
Definition	df-2nd 8013	Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 8021 proves that it does this. For example, (2nd ‘⟨3, 4⟩) = 4. Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 6249 and op2ndb 6248). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥})
Theorem	1stval 8014	The value of the function that extracts the first member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (1st ‘𝐴) = ∪ dom {𝐴}
Theorem	2ndval 8015	The value of the function that extracts the second member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (2nd ‘𝐴) = ∪ ran {𝐴}
Theorem	1stnpr 8016	Value of the first-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ (¬ 𝐴 ∈ (V × V) → (1st ‘𝐴) = ∅)
Theorem	2ndnpr 8017	Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ (¬ 𝐴 ∈ (V × V) → (2nd ‘𝐴) = ∅)
Theorem	1st0 8018	The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
⊢ (1st ‘∅) = ∅
Theorem	2nd0 8019	The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
⊢ (2nd ‘∅) = ∅
Theorem	op1st 8020	Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴
Theorem	op2nd 8021	Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
Theorem	op1std 8022	Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1st ‘𝐶) = 𝐴)
Theorem	op2ndd 8023	Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = 𝐵)
Theorem	op1stg 8024	Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)
Theorem	op2ndg 8025	Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)
Theorem	ot1stg 8026	Extract the first member of an ordered triple. (Due to infrequent usage, it isn't worthwhile at this point to define special extractors for triples, so we reuse the ordered pair extractors for ot1stg 8026, ot2ndg 8027, ot3rdg 8028.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (1st ‘(1st ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐴)
Theorem	ot2ndg 8027	Extract the second member of an ordered triple. (See ot1stg 8026 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2nd ‘(1st ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐵)
Theorem	ot3rdg 8028	Extract the third member of an ordered triple. (See ot1stg 8026 comment.) (Contributed by NM, 3-Apr-2015.)
⊢ (𝐶 ∈ 𝑉 → (2nd ‘⟨𝐴, 𝐵, 𝐶⟩) = 𝐶)
Theorem	1stval2 8029	Alternate value of the function that extracts the first member of an ordered pair. Definition 5.13 (i) of [Monk1] p. 52. (Contributed by NM, 18-Aug-2006.)
⊢ (𝐴 ∈ (V × V) → (1st ‘𝐴) = ∩ ∩ 𝐴)
Theorem	2ndval2 8030	Alternate value of the function that extracts the second member of an ordered pair. Definition 5.13 (ii) of [Monk1] p. 52. (Contributed by NM, 18-Aug-2006.)
⊢ (𝐴 ∈ (V × V) → (2nd ‘𝐴) = ∩ ∩ ∩ ◡{𝐴})
Theorem	oteqimp 8031	The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
⊢ (𝑇 = ⟨𝐴, 𝐵, 𝐶⟩ → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = 𝐵 ∧ (2nd ‘𝑇) = 𝐶)))
Theorem	fo1st 8032	The 1st function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ 1st :V–onto→V
Theorem	fo2nd 8033	The 2nd function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ 2nd :V–onto→V
Theorem	br1steqg 8034	Uniqueness condition for the binary relation 1st. (Contributed by Scott Fenton, 2-Jul-2020.) Revised to remove sethood hypothesis on 𝐶. (Revised by Peter Mazsa, 17-Jan-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩1st 𝐶 ↔ 𝐶 = 𝐴))
Theorem	br2ndeqg 8035	Uniqueness condition for the binary relation 2nd. (Contributed by Scott Fenton, 2-Jul-2020.) Revised to remove sethood hypothesis on 𝐶. (Revised by Peter Mazsa, 17-Jan-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩2nd 𝐶 ↔ 𝐶 = 𝐵))
Theorem	f1stres 8036	Mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 11-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐴
Theorem	f2ndres 8037	Mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 7-Aug-2006.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (2nd ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐵
Theorem	fo1stres 8038	Onto mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 14-Dec-2008.)
⊢ (𝐵 ≠ ∅ → (1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)–onto→𝐴)
Theorem	fo2ndres 8039	Onto mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 14-Dec-2008.)
⊢ (𝐴 ≠ ∅ → (2nd ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)–onto→𝐵)
Theorem	1st2val 8040*	Value of an alternate definition of the 1st function. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑧 = 𝑥}‘𝐴) = (1st ‘𝐴)
Theorem	2nd2val 8041*	Value of an alternate definition of the 2nd function. (Contributed by NM, 10-Aug-2006.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑧 = 𝑦}‘𝐴) = (2nd ‘𝐴)
Theorem	1stcof 8042	Composition of the first member function with another function. (Contributed by NM, 12-Oct-2007.)
⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (1st ∘ 𝐹):𝐴⟶𝐵)
Theorem	2ndcof 8043	Composition of the second member function with another function. (Contributed by FL, 15-Oct-2012.)
⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (2nd ∘ 𝐹):𝐴⟶𝐶)
Theorem	xp1st 8044	Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)
Theorem	xp2nd 8045	Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
Theorem	elxp6 8046	Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7944. (Contributed by NM, 9-Oct-2004.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶)))
Theorem	elxp7 8047	Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7944. (Contributed by NM, 19-Aug-2006.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 ∈ (V × V) ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶)))
Theorem	eqopi 8048	Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.) (Revised by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝐴 ∈ (𝑉 × 𝑊) ∧ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶)) → 𝐴 = ⟨𝐵, 𝐶⟩)
Theorem	xp2 8049*	Representation of Cartesian product based on ordered pair component functions. (Contributed by NM, 16-Sep-2006.)
⊢ (𝐴 × 𝐵) = {𝑥 ∈ (V × V) ∣ ((1st ‘𝑥) ∈ 𝐴 ∧ (2nd ‘𝑥) ∈ 𝐵)}
Theorem	unielxp 8050	The membership relation for a Cartesian product is inherited by union. (Contributed by NM, 16-Sep-2006.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∪ 𝐴 ∈ ∪ (𝐵 × 𝐶))
Theorem	1st2nd2 8051	Reconstruction of a member of a Cartesian product in terms of its ordered pair components. (Contributed by NM, 20-Oct-2013.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
Theorem	1st2ndb 8052	Reconstruction of an ordered pair in terms of its components. (Contributed by NM, 25-Feb-2014.)
⊢ (𝐴 ∈ (V × V) ↔ 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
Theorem	xpopth 8053	An ordered pair theorem for members of Cartesian products. (Contributed by NM, 20-Jun-2007.)
⊢ ((𝐴 ∈ (𝐶 × 𝐷) ∧ 𝐵 ∈ (𝑅 × 𝑆)) → (((1st ‘𝐴) = (1st ‘𝐵) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) ↔ 𝐴 = 𝐵))
Theorem	eqop 8054	Two ways to express equality with an ordered pair. (Contributed by NM, 3-Sep-2007.) (Proof shortened by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ∈ (𝑉 × 𝑊) → (𝐴 = ⟨𝐵, 𝐶⟩ ↔ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶)))
Theorem	eqop2 8055	Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 = ⟨𝐵, 𝐶⟩ ↔ (𝐴 ∈ (V × V) ∧ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶)))
Theorem	op1steq 8056*	Two ways of expressing that an element is the first member of an ordered pair. (Contributed by NM, 22-Sep-2013.) (Revised by Mario Carneiro, 23-Feb-2014.)
⊢ (𝐴 ∈ (𝑉 × 𝑊) → ((1st ‘𝐴) = 𝐵 ↔ ∃𝑥 𝐴 = ⟨𝐵, 𝑥⟩))
Theorem	opreuopreu 8057*	There is a unique ordered pair fulfilling a wff iff its components fulfil a corresponding wff. (Contributed by AV, 2-Jul-2023.)
⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → (𝜓 ↔ 𝜑))    ⇒   ⊢ (∃!𝑝 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃!𝑝 ∈ (𝐴 × 𝐵)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜓))
Theorem	el2xptp 8058*	A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
⊢ (𝐴 ∈ ((𝐵 × 𝐶) × 𝐷) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝐴 = ⟨𝑥, 𝑦, 𝑧⟩)
Theorem	el2xptp0 8059	A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((𝐴 ∈ ((𝑈 × 𝑉) × 𝑊) ∧ ((1st ‘(1st ‘𝐴)) = 𝑋 ∧ (2nd ‘(1st ‘𝐴)) = 𝑌 ∧ (2nd ‘𝐴) = 𝑍)) ↔ 𝐴 = ⟨𝑋, 𝑌, 𝑍⟩))
Theorem	el2xpss 8060*	Version of elrel 5810 for triple Cartesian products. (Contributed by Scott Fenton, 1-Feb-2025.)
⊢ ((𝐴 ∈ 𝑅 ∧ 𝑅 ⊆ ((𝐵 × 𝐶) × 𝐷)) → ∃𝑥∃𝑦∃𝑧 𝐴 = ⟨𝑥, 𝑦, 𝑧⟩)
Theorem	2nd1st 8061	Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∪ ◡{𝐴} = ⟨(2nd ‘𝐴), (1st ‘𝐴)⟩)
Theorem	1st2nd 8062	Reconstruction of a member of a relation in terms of its ordered pair components. (Contributed by NM, 29-Aug-2006.)
⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
Theorem	1stdm 8063	The first ordered pair component of a member of a relation belongs to the domain of the relation. (Contributed by NM, 17-Sep-2006.)
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → (1st ‘𝐴) ∈ dom 𝑅)
Theorem	2ndrn 8064	The second ordered pair component of a member of a relation belongs to the range of the relation. (Contributed by NM, 17-Sep-2006.)
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → (2nd ‘𝐴) ∈ ran 𝑅)
Theorem	1st2ndbr 8065	Express an element of a relation as a relationship between first and second components. (Contributed by Mario Carneiro, 22-Jun-2016.)
⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → (1st ‘𝐴)𝐵(2nd ‘𝐴))
Theorem	releldm2 8066*	Two ways of expressing membership in the domain of a relation. (Contributed by NM, 22-Sep-2013.)
⊢ (Rel 𝐴 → (𝐵 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵))
Theorem	reldm 8067*	An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013.)
⊢ (Rel 𝐴 → dom 𝐴 = ran (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥)))
Theorem	releldmdifi 8068*	One way of expressing membership in the difference of domains of two nested relations. (Contributed by AV, 26-Oct-2023.)
⊢ ((Rel 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (dom 𝐴 ∖ dom 𝐵) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶))
Theorem	funfv1st2nd 8069	The function value for the first component of an ordered pair is the second component of the ordered pair. (Contributed by AV, 17-Oct-2023.)
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ 𝐹) → (𝐹‘(1st ‘𝑋)) = (2nd ‘𝑋))
Theorem	funelss 8070	If the first component of an element of a function is in the domain of a subset of the function, the element is a member of this subset. (Contributed by AV, 27-Oct-2023.)
⊢ ((Fun 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑋 ∈ 𝐴) → ((1st ‘𝑋) ∈ dom 𝐵 → 𝑋 ∈ 𝐵))
Theorem	funeldmdif 8071*	Two ways of expressing membership in the difference of domains of two nested functions. (Contributed by AV, 27-Oct-2023.)
⊢ ((Fun 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (dom 𝐴 ∖ dom 𝐵) ↔ ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶))
Theorem	sbcopeq1a 8072	Equality theorem for substitution of a class for an ordered pair (analogue of sbceq1a 3801 that avoids the existential quantifiers of copsexg 5501). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ([(1st ‘𝐴) / 𝑥][(2nd ‘𝐴) / 𝑦]𝜑 ↔ 𝜑))
Theorem	csbopeq1a 8073	Equality theorem for substitution of a class 𝐴 for an ordered pair ⟨𝑥, 𝑦⟩ in 𝐵 (analogue of csbeq1a 3921). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ⦋(1st ‘𝐴) / 𝑥⦌⦋(2nd ‘𝐴) / 𝑦⦌𝐵 = 𝐵)
Theorem	sbcoteq1a 8074	Equality theorem for substitution of a class for an ordered triple. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ (𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ → ([(1st ‘(1st ‘𝐴)) / 𝑥][(2nd ‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑 ↔ 𝜑))
Theorem	dfopab2 8075*	A way to define an ordered-pair class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∈ (V × V) ∣ [(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑}
Theorem	dfoprab3s 8076*	A way to define an operation class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ (V × V) ∧ [(1st ‘𝑤) / 𝑥][(2nd ‘𝑤) / 𝑦]𝜑)}
Theorem	dfoprab3 8077*	Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008.)
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ (V × V) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
Theorem	dfoprab4 8078*	Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}
Theorem	dfoprab4f 8079*	Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 20-Dec-2008.) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}
Theorem	opabex2 8080*	Condition for an operation to be a set. (Contributed by Thierry Arnoux, 25-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑥 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑦 ∈ 𝐵)    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} ∈ V)
Theorem	opabn1stprc 8081*	An ordered-pair class abstraction which does not depend on the first abstraction variable is a proper class. There must be, however, at least one set which satisfies the restricting wff. (Contributed by AV, 27-Dec-2020.)
⊢ (∃𝑦𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∉ V)
Theorem	opiota 8082*	The property of a uniquely specified ordered pair. The proof uses properties of the ℩ description binder. (Contributed by Mario Carneiro, 21-May-2015.)
⊢ 𝐼 = (℩𝑧∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))    &   ⊢ 𝑋 = (1st ‘𝐼)    &   ⊢ 𝑌 = (2nd ‘𝐼)    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐷 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃!𝑧∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝜒) ↔ (𝐶 = 𝑋 ∧ 𝐷 = 𝑌)))
Theorem	cnvoprab 8083*	The converse of a class abstraction of nested ordered pairs. (Contributed by Thierry Arnoux, 17-Aug-2017.) (Proof shortened by Thierry Arnoux, 20-Feb-2022.)
⊢ (𝑎 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜑))    &   ⊢ (𝜓 → 𝑎 ∈ (V × V))    ⇒   ⊢ ◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑧, 𝑎⟩ ∣ 𝜓}
Theorem	dfxp3 8084*	Define the Cartesian product of three classes. Compare df-xp 5694. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 3-Nov-2015.)
⊢ ((𝐴 × 𝐵) × 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)}
Theorem	elopabi 8085*	A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006.)
⊢ (𝑥 = (1st ‘𝐴) → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = (2nd ‘𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → 𝜒)
Theorem	eloprabi 8086*	A consequence of membership in an operation class abstraction, using ordered pair extractors. (Contributed by NM, 6-Nov-2006.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝑥 = (1st ‘(1st ‘𝐴)) → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = (2nd ‘(1st ‘𝐴)) → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = (2nd ‘𝐴) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝐴 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} → 𝜃)
Theorem	mpomptsx 8087*	Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd ‘𝑧) / 𝑦⦌𝐶)
Theorem	mpompts 8088*	Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd ‘𝑧) / 𝑦⦌𝐶)
Theorem	dmmpossx 8089*	The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ dom 𝐹 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
Theorem	fmpox 8090*	Functionality, domain and codomain of a class given by the maps-to notation, where 𝐵(𝑥) is not constant but depends on 𝑥. (Contributed by NM, 29-Dec-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷)
Theorem	fmpo 8091*	Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷)
Theorem	fnmpo 8092*	Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → 𝐹 Fn (𝐴 × 𝐵))
Theorem	fnmpoi 8093*	Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ 𝐹 Fn (𝐴 × 𝐵)
Theorem	dmmpo 8094*	Domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ dom 𝐹 = (𝐴 × 𝐵)
Theorem	ovmpoelrn 8095*	An operation's value belongs to its range. (Contributed by AV, 27-Jan-2020.)
⊢ 𝑂 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝑂𝑌) ∈ 𝑀)
Theorem	dmmpoga 8096*	Domain of an operation given by the maps-to notation, closed form of dmmpo 8094. (Contributed by Alexander van der Vekens, 10-Feb-2019.) (Proof shortened by Lammen, 29-May-2024.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → dom 𝐹 = (𝐴 × 𝐵))
Theorem	dmmpog 8097*	Domain of an operation given by the maps-to notation, closed form of dmmpo 8094. Caution: This theorem is only valid in the very special case where the value of the mapping is a constant! (Contributed by Alexander van der Vekens, 1-Jun-2017.) (Proof shortened by AV, 10-Feb-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (𝐶 ∈ 𝑉 → dom 𝐹 = (𝐴 × 𝐵))
Theorem	mpoexxg 8098*	Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑆) → 𝐹 ∈ V)
Theorem	mpoexg 8099*	Existence of an operation class abstraction (special case). (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → 𝐹 ∈ V)
Theorem	mpoexga 8100*	If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by NM, 12-Sep-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V)