P. 63 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6201-6300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	off 6201*	The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝐴 ∩ 𝐵) = 𝐶    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺):𝐶⟶𝑈)
Theorem	offeq 6202*	Convert an identity of the operation to the analogous identity on the function operation. (Contributed by Jim Kingdon, 26-Nov-2023.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝐴 ∩ 𝐵) = 𝐶    &   ⊢ (𝜑 → 𝐻:𝐶⟶𝑈)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐸)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐷𝑅𝐸) = (𝐻‘𝑥))    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = 𝐻)
Theorem	ofres 6203	Restrict the operands of a function operation to the same domain as that of the operation itself. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝐴 ∩ 𝐵) = 𝐶    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = ((𝐹 ↾ 𝐶) ∘𝑓 𝑅(𝐺 ↾ 𝐶)))
Theorem	offval2 6204*	The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶))    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶)))
Theorem	ofrfval2 6205*	The function relation acting on maps. (Contributed by Mario Carneiro, 20-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶))    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑟 𝑅𝐺 ↔ ∀𝑥 ∈ 𝐴 𝐵𝑅𝐶))
Theorem	suppssof1 6206*	Formula building theorem for support restrictions: vector operation with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ (𝜑 → (◡𝐴 “ (V ∖ {𝑌})) ⊆ 𝐿)    &   ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍)    &   ⊢ (𝜑 → 𝐴:𝐷⟶𝑉)    &   ⊢ (𝜑 → 𝐵:𝐷⟶𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (◡(𝐴 ∘𝑓 𝑂𝐵) “ (V ∖ {𝑍})) ⊆ 𝐿)
Theorem	ofco 6207	The composition of a function operation with another function. (Contributed by Mario Carneiro, 19-Dec-2014.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    &   ⊢ (𝜑 → 𝐻:𝐷⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝐴 ∩ 𝐵) = 𝐶    ⇒   ⊢ (𝜑 → ((𝐹 ∘𝑓 𝑅𝐺) ∘ 𝐻) = ((𝐹 ∘ 𝐻) ∘𝑓 𝑅(𝐺 ∘ 𝐻)))
Theorem	offveqb 6208*	Equivalent expressions for equality with a function operation. (Contributed by NM, 9-Oct-2014.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐴)    &   ⊢ (𝜑 → 𝐻 Fn 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐻 = (𝐹 ∘𝑓 𝑅𝐺) ↔ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐵𝑅𝐶)))
Theorem	offveq 6209*	Convert an identity of the operation to the analogous identity on the function operation. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐴)    &   ⊢ (𝜑 → 𝐻 Fn 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵𝑅𝐶) = (𝐻‘𝑥))    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = 𝐻)
Theorem	ofc1g 6210	Left operation by a constant. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐵𝑅𝐶) ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (((𝐴 × {𝐵}) ∘𝑓 𝑅𝐹)‘𝑋) = (𝐵𝑅𝐶))
Theorem	ofc2g 6211	Right operation by a constant. (Contributed by NM, 7-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐶𝑅𝐵) ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘𝑓 𝑅(𝐴 × {𝐵}))‘𝑋) = (𝐶𝑅𝐵))
Theorem	ofc12 6212	Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 𝑅(𝐴 × {𝐶})) = (𝐴 × {(𝐵𝑅𝐶)}))
Theorem	caofref 6213*	Transfer a reflexive law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥𝑅𝑥)    ⇒   ⊢ (𝜑 → 𝐹 ∘𝑟 𝑅𝐹)
Theorem	caofinvl 6214*	Transfer a left inverse law to the function operation. (Contributed by NM, 22-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑁:𝑆⟶𝑆)    &   ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣))))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑁‘𝑥)𝑅𝑥) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐺 ∘𝑓 𝑅𝐹) = (𝐴 × {𝐵}))
Theorem	caofid0l 6215*	Transfer a left identity law to the function operation. (Contributed by NM, 21-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐵𝑅𝑥) = 𝑥)    ⇒   ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 𝑅𝐹) = 𝐹)
Theorem	caofid0r 6216*	Transfer a right identity law to the function operation. (Contributed by NM, 21-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥𝑅𝐵) = 𝑥)    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅(𝐴 × {𝐵})) = 𝐹)
Theorem	caofid1 6217*	Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥𝑅𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅(𝐴 × {𝐵})) = (𝐴 × {𝐶}))
Theorem	caofid2 6218*	Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐵𝑅𝑥) = 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 𝑅𝐹) = (𝐴 × {𝐶}))
Theorem	caofcom 6219*	Transfer a commutative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦) = (𝑦𝑅𝑥))    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝐺 ∘𝑓 𝑅𝐹))
Theorem	caofrss 6220*	Transfer a relation subset law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦 → 𝑥𝑇𝑦))    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑟 𝑅𝐺 → 𝐹 ∘𝑟 𝑇𝐺))
Theorem	caoftrn 6221*	Transfer a transitivity law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐻:𝐴⟶𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) → 𝑥𝑈𝑧))    ⇒   ⊢ (𝜑 → ((𝐹 ∘𝑟 𝑅𝐺 ∧ 𝐺 ∘𝑟 𝑇𝐻) → 𝐹 ∘𝑟 𝑈𝐻))
Theorem	caofdig 6222*	Transfer a distributive law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐾)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐻:𝐴⟶𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦) ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑇𝑦) ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑇(𝑦𝑅𝑧)) = ((𝑥𝑇𝑦)𝑂(𝑥𝑇𝑧)))    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 𝑇(𝐺 ∘𝑓 𝑅𝐻)) = ((𝐹 ∘𝑓 𝑇𝐺) ∘𝑓 𝑂(𝐹 ∘𝑓 𝑇𝐻)))
2.6.14  Functions (continued)
Theorem	resfunexgALT 6223	The restriction of a function to a set exists. Compare Proposition 6.17 of [TakeutiZaring] p. 28. This version has a shorter proof than resfunexg 5833 but requires ax-pow 4237 and ax-un 4501. (Contributed by NM, 7-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V)
Theorem	cofunexg 6224	Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∘ 𝐵) ∈ V)
Theorem	cofunex2g 6225	Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007.)
⊢ ((𝐴 ∈ 𝑉 ∧ Fun ◡𝐵) → (𝐴 ∘ 𝐵) ∈ V)
Theorem	fnexALT 6226	If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of funimaexg 5381. This version of fnex 5834 uses ax-pow 4237 and ax-un 4501, whereas fnex 5834 does not. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V)
Theorem	funexw 6227	Weak version of funex 5835 that holds without ax-coll 4178. If the domain and codomain of a function exist, so does the function. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ ((Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵 ∧ ran 𝐹 ∈ 𝐶) → 𝐹 ∈ V)
Theorem	mptexw 6228*	Weak version of mptex 5838 that holds without ax-coll 4178. If the domain and codomain of a function given by maps-to notation are sets, the function is a set. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V
Theorem	funrnex 6229	If the domain of a function exists, so does its range. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of funex 5835. (Contributed by NM, 11-Nov-1995.)
⊢ (dom 𝐹 ∈ 𝐵 → (Fun 𝐹 → ran 𝐹 ∈ V))
Theorem	focdmex 6230	If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004.)
⊢ (𝐴 ∈ 𝐶 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V))
Theorem	f1dmex 6231	If the codomain of a one-to-one function exists, so does its domain. This can be thought of as a form of the Axiom of Replacement. (Contributed by NM, 4-Sep-2004.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
Theorem	abrexex 6232*	Existence of a class abstraction of existentially restricted sets. 𝑥 is normally a free-variable parameter in the class expression substituted for 𝐵, which can be thought of as 𝐵(𝑥). This simple-looking theorem is actually quite powerful and appears to involve the Axiom of Replacement in an intrinsic way, as can be seen by tracing back through the path mptexg 5837, funex 5835, fnex 5834, resfunexg 5833, and funimaexg 5381. See also abrexex2 6239. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V
Theorem	abrexexg 6233*	Existence of a class abstraction of existentially restricted sets. 𝑥 is normally a free-variable parameter in 𝐵. The antecedent assures us that 𝐴 is a set. (Contributed by NM, 3-Nov-2003.)
⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
Theorem	iunexg 6234*	The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵. (Contributed by NM, 23-Mar-2006.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
Theorem	abrexex2g 6235*	Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V)
Theorem	opabex3d 6236*	Existence of an ordered pair abstraction, deduction version. (Contributed by Alexander van der Vekens, 19-Oct-2017.)
⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝜓} ∈ V)    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} ∈ V)
Theorem	opabex3 6237*	Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → {𝑦 ∣ 𝜑} ∈ V)    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V
Theorem	iunex 6238*	The existence of an indexed union. 𝑥 is normally a free-variable parameter in the class expression substituted for 𝐵, which can be read informally as 𝐵(𝑥). (Contributed by NM, 13-Oct-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V
Theorem	abrexex2 6239*	Existence of an existentially restricted class abstraction. 𝜑 is normally has free-variable parameters 𝑥 and 𝑦. See also abrexex 6232. (Contributed by NM, 12-Sep-2004.)
⊢ 𝐴 ∈ V    &   ⊢ {𝑦 ∣ 𝜑} ∈ V    ⇒   ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V
Theorem	abexssex 6240*	Existence of a class abstraction with an existentially quantified expression. Both 𝑥 and 𝑦 can be free in 𝜑. (Contributed by NM, 29-Jul-2006.)
⊢ 𝐴 ∈ V    &   ⊢ {𝑦 ∣ 𝜑} ∈ V    ⇒   ⊢ {𝑦 ∣ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝜑)} ∈ V
Theorem	abexex 6241*	A condition where a class builder continues to exist after its wff is existentially quantified. (Contributed by NM, 4-Mar-2007.)
⊢ 𝐴 ∈ V    &   ⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ {𝑦 ∣ 𝜑} ∈ V    ⇒   ⊢ {𝑦 ∣ ∃𝑥𝜑} ∈ V
Theorem	oprabexd 6242*	Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑧𝜓)    &   ⊢ (𝜑 → 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)})    ⇒   ⊢ (𝜑 → 𝐹 ∈ V)
Theorem	oprabex 6243*	Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃*𝑧𝜑)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)}    ⇒   ⊢ 𝐹 ∈ V
Theorem	oprabex3 6244*	Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004.)
⊢ 𝐻 ∈ V    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}    ⇒   ⊢ 𝐹 ∈ V
Theorem	oprabrexex2 6245*	Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.)
⊢ 𝐴 ∈ V    &   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ∈ V    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑤 ∈ 𝐴 𝜑} ∈ V
Theorem	ab2rexex 6246*	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 6232. (Contributed by NM, 20-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} ∈ V
Theorem	ab2rexex2 6247*	Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥, 𝑦, and 𝑧. Compare abrexex2 6239. (Contributed by NM, 20-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ {𝑧 ∣ 𝜑} ∈ V    ⇒   ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} ∈ V
Theorem	xpexgALT 6248	The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. This version is proven using Replacement; see xpexg 4810 for a version that uses the Power Set axiom instead. (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
Theorem	offval3 6249*	General value of (𝐹 ∘𝑓 𝑅𝐺) with no assumptions on functionality of 𝐹 and 𝐺. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))))
Theorem	offres 6250	Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘𝑓 𝑅𝐺) ↾ 𝐷) = ((𝐹 ↾ 𝐷) ∘𝑓 𝑅(𝐺 ↾ 𝐷)))
Theorem	ofmres 6251*	Equivalent expressions for a restriction of the function operation map. Unlike ∘𝑓 𝑅 which is a proper class, ( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵)) can be a set by ofmresex 6252, allowing it to be used as a function or structure argument. By ofmresval 6200, the restricted operation map values are the same as the original values, allowing theorems for ∘𝑓 𝑅 to be reused. (Contributed by NM, 20-Oct-2014.)
⊢ ( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵)) = (𝑓 ∈ 𝐴, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘𝑓 𝑅𝑔))
Theorem	ofmresex 6252	Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵)) ∈ V)
Theorem	uchoice 6253*	Principle of unique choice. This is also called non-choice. The name choice results in its similarity to something like acfun 7357 (with the key difference being the change of ∃ to ∃!) but unique choice in fact follows from the axiom of collection and our other axioms. This is somewhat similar to Corollary 3.9.2 of [HoTT], p. (varies) but is better described by the paragraph at the end of Section 3.9 which starts "A similar issue arises in set-theoretic mathematics". (Contributed by Jim Kingdon, 13-Sep-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦𝜑) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑))
2.6.15  First and second members of an ordered pair
Syntax	c1st 6254	Extend the definition of a class to include the first member an ordered pair function.
class 1st
Syntax	c2nd 6255	Extend the definition of a class to include the second member an ordered pair function.
class 2nd
Definition	df-1st 6256	Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 6262 proves that it does this. For example, (1st ‘⟨ 3 , 4 ⟩) = 3 . Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 5186 and op1stb 4546). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
Definition	df-2nd 6257	Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 6263 proves that it does this. For example, (2nd ‘⟨ 3 , 4 ⟩) = 4 . Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 5189 and op2ndb 5188). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥})
Theorem	1stvalg 6258	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.)
⊢ (𝐴 ∈ V → (1st ‘𝐴) = ∪ dom {𝐴})
Theorem	2ndvalg 6259	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.)
⊢ (𝐴 ∈ V → (2nd ‘𝐴) = ∪ ran {𝐴})
Theorem	1st0 6260	The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
⊢ (1st ‘∅) = ∅
Theorem	2nd0 6261	The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
⊢ (2nd ‘∅) = ∅
Theorem	op1st 6262	Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴
Theorem	op2nd 6263	Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
Theorem	op1std 6264	Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1st ‘𝐶) = 𝐴)
Theorem	op2ndd 6265	Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2nd ‘𝐶) = 𝐵)
Theorem	op1stg 6266	Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)
Theorem	op2ndg 6267	Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵)
Theorem	ot1stg 6268	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 6268, ot2ndg 6269, ot3rdgg 6270.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (1st ‘(1st ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐴)
Theorem	ot2ndg 6269	Extract the second member of an ordered triple. (See ot1stg 6268 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2nd ‘(1st ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐵)
Theorem	ot3rdgg 6270	Extract the third member of an ordered triple. (See ot1stg 6268 comment.) (Contributed by NM, 3-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2nd ‘⟨𝐴, 𝐵, 𝐶⟩) = 𝐶)
Theorem	1stval2 6271	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 6272	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	fo1st 6273	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 6274	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	f1stres 6275	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 6276	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	fo1stresm 6277*	Onto mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
⊢ (∃𝑦 𝑦 ∈ 𝐵 → (1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)–onto→𝐴)
Theorem	fo2ndresm 6278*	Onto mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (2nd ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)–onto→𝐵)
Theorem	1stcof 6279	Composition of the first member function with another function. (Contributed by NM, 12-Oct-2007.)
⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (1st ∘ 𝐹):𝐴⟶𝐵)
Theorem	2ndcof 6280	Composition of the second member function with another function. (Contributed by FL, 15-Oct-2012.)
⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (2nd ∘ 𝐹):𝐴⟶𝐶)
Theorem	xp1st 6281	Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)
Theorem	xp2nd 6282	Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
Theorem	1stexg 6283	Existence of the first member of a set. (Contributed by Jim Kingdon, 26-Jan-2019.)
⊢ (𝐴 ∈ 𝑉 → (1st ‘𝐴) ∈ V)
Theorem	2ndexg 6284	Existence of the first member of a set. (Contributed by Jim Kingdon, 26-Jan-2019.)
⊢ (𝐴 ∈ 𝑉 → (2nd ‘𝐴) ∈ V)
Theorem	elxp6 6285	Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp4 5192. (Contributed by NM, 9-Oct-2004.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶)))
Theorem	elxp7 6286	Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp4 5192. (Contributed by NM, 19-Aug-2006.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 ∈ (V × V) ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶)))
Theorem	oprssdmm 6287*	Domain of closure of an operation. (Contributed by Jim Kingdon, 23-Oct-2023.)
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ∃𝑣 𝑣 ∈ 𝑢)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → Rel 𝐹)    ⇒   ⊢ (𝜑 → (𝑆 × 𝑆) ⊆ dom 𝐹)
Theorem	eqopi 6288	Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.) (Revised by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝐴 ∈ (𝑉 × 𝑊) ∧ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶)) → 𝐴 = ⟨𝐵, 𝐶⟩)
Theorem	xp2 6289*	Representation of cross product based on ordered pair component functions. (Contributed by NM, 16-Sep-2006.)
⊢ (𝐴 × 𝐵) = {𝑥 ∈ (V × V) ∣ ((1st ‘𝑥) ∈ 𝐴 ∧ (2nd ‘𝑥) ∈ 𝐵)}
Theorem	unielxp 6290	The membership relation for a cross product is inherited by union. (Contributed by NM, 16-Sep-2006.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∪ 𝐴 ∈ ∪ (𝐵 × 𝐶))
Theorem	1st2nd2 6291	Reconstruction of a member of a cross product in terms of its ordered pair components. (Contributed by NM, 20-Oct-2013.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
Theorem	xpopth 6292	An ordered pair theorem for members of cross products. (Contributed by NM, 20-Jun-2007.)
⊢ ((𝐴 ∈ (𝐶 × 𝐷) ∧ 𝐵 ∈ (𝑅 × 𝑆)) → (((1st ‘𝐴) = (1st ‘𝐵) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) ↔ 𝐴 = 𝐵))
Theorem	eqop 6293	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 6294	Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 = ⟨𝐵, 𝐶⟩ ↔ (𝐴 ∈ (V × V) ∧ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶)))
Theorem	op1steq 6295*	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	2nd1st 6296	Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∪ ◡{𝐴} = ⟨(2nd ‘𝐴), (1st ‘𝐴)⟩)
Theorem	1st2nd 6297	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 6298	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 6299	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 6300	Express an element of a relation as a relationship between first and second components. (Contributed by Mario Carneiro, 22-Jun-2016.)
⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → (1st ‘𝐴)𝐵(2nd ‘𝐴))