Type  Label  Description 
Statement 

Theorem  off 6001* 
The function operation produces a function. (Contributed by Mario
Carneiro, 20Jul2014.)

⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → (𝐹 ∘_{𝑓} 𝑅𝐺):𝐶⟶𝑈) 

Theorem  offeq 6002* 
Convert an identity of the operation to the analogous identity on
the function operation. (Contributed by Jim Kingdon,
26Nov2023.)

⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶
& ⊢ (𝜑 → 𝐻:𝐶⟶𝑈)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐷)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐸)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐷𝑅𝐸) = (𝐻‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘_{𝑓} 𝑅𝐺) = 𝐻) 

Theorem  ofres 6003 
Restrict the operands of a function operation to the same domain as that
of the operation itself. (Contributed by Mario Carneiro,
15Sep2014.)

⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → (𝐹 ∘_{𝑓} 𝑅𝐺) = ((𝐹 ↾ 𝐶) ∘_{𝑓} 𝑅(𝐺 ↾ 𝐶))) 

Theorem  offval2 6004* 
The function operation expressed as a mapping. (Contributed by Mario
Carneiro, 20Jul2014.)

⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘_{𝑓} 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) 

Theorem  ofrfval2 6005* 
The function relation acting on maps. (Contributed by Mario Carneiro,
20Jul2014.)

⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘_{𝑟} 𝑅𝐺 ↔ ∀𝑥 ∈ 𝐴 𝐵𝑅𝐶)) 

Theorem  suppssof1 6006* 
Formula building theorem for support restrictions: vector operation with
left annihilator. (Contributed by Stefan O'Rear, 9Mar2015.)

⊢ (𝜑 → (^{◡}𝐴 “ (V ∖ {𝑌})) ⊆ 𝐿)
& ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍)
& ⊢ (𝜑 → 𝐴:𝐷⟶𝑉)
& ⊢ (𝜑 → 𝐵:𝐷⟶𝑅)
& ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (^{◡}(𝐴 ∘_{𝑓} 𝑂𝐵) “ (V ∖ {𝑍})) ⊆ 𝐿) 

Theorem  ofco 6007 
The composition of a function operation with another function.
(Contributed by Mario Carneiro, 19Dec2014.)

⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐻:𝐷⟶𝐶)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝐷 ∈ 𝑋)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → ((𝐹 ∘_{𝑓} 𝑅𝐺) ∘ 𝐻) = ((𝐹 ∘ 𝐻) ∘_{𝑓} 𝑅(𝐺 ∘ 𝐻))) 

Theorem  offveqb 6008* 
Equivalent expressions for equality with a function operation.
(Contributed by NM, 9Oct2014.) (Proof shortened by Mario Carneiro,
5Dec2016.)

⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐴)
& ⊢ (𝜑 → 𝐻 Fn 𝐴)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = 𝐶) ⇒ ⊢ (𝜑 → (𝐻 = (𝐹 ∘_{𝑓} 𝑅𝐺) ↔ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐵𝑅𝐶))) 

Theorem  ofc12 6009 
Function operation on two constant functions. (Contributed by Mario
Carneiro, 28Jul2014.)

⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘_{𝑓} 𝑅(𝐴 × {𝐶})) = (𝐴 × {(𝐵𝑅𝐶)})) 

Theorem  caofref 6010* 
Transfer a reflexive law to the function relation. (Contributed by
Mario Carneiro, 28Jul2014.)

⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥𝑅𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∘_{𝑟} 𝑅𝐹) 

Theorem  caofinvl 6011* 
Transfer a left inverse law to the function operation. (Contributed
by NM, 22Oct2014.)

⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝑁:𝑆⟶𝑆)
& ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣)))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑁‘𝑥)𝑅𝑥) = 𝐵) ⇒ ⊢ (𝜑 → (𝐺 ∘_{𝑓} 𝑅𝐹) = (𝐴 × {𝐵})) 

Theorem  caofcom 6012* 
Transfer a commutative law to the function operation. (Contributed by
Mario Carneiro, 26Jul2014.)

⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦) = (𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘_{𝑓} 𝑅𝐺) = (𝐺 ∘_{𝑓} 𝑅𝐹)) 

Theorem  caofrss 6013* 
Transfer a relation subset law to the function relation. (Contributed
by Mario Carneiro, 28Jul2014.)

⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦 → 𝑥𝑇𝑦)) ⇒ ⊢ (𝜑 → (𝐹 ∘_{𝑟} 𝑅𝐺 → 𝐹 ∘_{𝑟} 𝑇𝐺)) 

Theorem  caoftrn 6014* 
Transfer a transitivity law to the function relation. (Contributed by
Mario Carneiro, 28Jul2014.)

⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐻:𝐴⟶𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) → 𝑥𝑈𝑧)) ⇒ ⊢ (𝜑 → ((𝐹 ∘_{𝑟} 𝑅𝐺 ∧ 𝐺 ∘_{𝑟} 𝑇𝐻) → 𝐹 ∘_{𝑟} 𝑈𝐻)) 

2.6.13 Functions (continued)


Theorem  resfunexgALT 6015 
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 5648 but requires axpow 4105 and axun 4362. (Contributed by NM,
7Apr1995.) (Proof modification is discouraged.)
(New usage is discouraged.)

⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) 

Theorem  cofunexg 6016 
Existence of a composition when the first member is a function.
(Contributed by NM, 8Oct2007.)

⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∘ 𝐵) ∈ V) 

Theorem  cofunex2g 6017 
Existence of a composition when the second member is onetoone.
(Contributed by NM, 8Oct2007.)

⊢ ((𝐴 ∈ 𝑉 ∧ Fun ^{◡}𝐵) → (𝐴 ∘ 𝐵) ∈ V) 

Theorem  fnexALT 6018 
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 5214. This version of fnex 5649
uses
axpow 4105 and axun 4362, whereas fnex 5649
does not. (Contributed by NM,
14Aug1994.) (Proof modification is discouraged.)
(New usage is discouraged.)

⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) 

Theorem  funrnex 6019 
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 5650. (Contributed by NM, 11Nov1995.)

⊢ (dom 𝐹 ∈ 𝐵 → (Fun 𝐹 → ran 𝐹 ∈ V)) 

Theorem  fornex 6020 
If the domain of an onto function exists, so does its codomain.
(Contributed by NM, 23Jul2004.)

⊢ (𝐴 ∈ 𝐶 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V)) 

Theorem  f1dmex 6021 
If the codomain of a onetoone function exists, so does its domain. This
can be thought of as a form of the Axiom of Replacement. (Contributed by
NM, 4Sep2004.)

⊢ ((𝐹:𝐴–11→𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) 

Theorem  abrexex 6022* 
Existence of a class abstraction of existentially restricted sets. 𝑥
is normally a freevariable parameter in the class expression
substituted for 𝐵, which can be thought of as 𝐵(𝑥). This
simplelooking 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 5652, funex 5650, fnex 5649, resfunexg 5648, and
funimaexg 5214. See also abrexex2 6029. (Contributed by NM, 16Oct2003.)
(Proof shortened by Mario Carneiro, 31Aug2015.)

⊢ 𝐴 ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V 

Theorem  abrexexg 6023* 
Existence of a class abstraction of existentially restricted sets. 𝑥
is normally a freevariable parameter in 𝐵. The antecedent assures
us that 𝐴 is a set. (Contributed by NM,
3Nov2003.)

⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) 

Theorem  iunexg 6024* 
The existence of an indexed union. 𝑥 is normally a freevariable
parameter in 𝐵. (Contributed by NM, 23Mar2006.)

⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) 

Theorem  abrexex2g 6025* 
Existence of an existentially restricted class abstraction.
(Contributed by Jeff Madsen, 2Sep2009.)

⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V) 

Theorem  opabex3d 6026* 
Existence of an ordered pair abstraction, deduction version.
(Contributed by Alexander van der Vekens, 19Oct2017.)

⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝜓} ∈ V) ⇒ ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} ∈ V) 

Theorem  opabex3 6027* 
Existence of an ordered pair abstraction. (Contributed by Jeff Madsen,
2Sep2009.)

⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → {𝑦 ∣ 𝜑} ∈ V) ⇒ ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V 

Theorem  iunex 6028* 
The existence of an indexed union. 𝑥 is normally a freevariable
parameter in the class expression substituted for 𝐵, which can be
read informally as 𝐵(𝑥). (Contributed by NM, 13Oct2003.)

⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V 

Theorem  abrexex2 6029* 
Existence of an existentially restricted class abstraction. 𝜑 is
normally has freevariable parameters 𝑥 and 𝑦. See
also
abrexex 6022. (Contributed by NM, 12Sep2004.)

⊢ 𝐴 ∈ V & ⊢ {𝑦 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V 

Theorem  abexssex 6030* 
Existence of a class abstraction with an existentially quantified
expression. Both 𝑥 and 𝑦 can be free in 𝜑.
(Contributed
by NM, 29Jul2006.)

⊢ 𝐴 ∈ V & ⊢ {𝑦 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝜑)} ∈ V 

Theorem  abexex 6031* 
A condition where a class builder continues to exist after its wff is
existentially quantified. (Contributed by NM, 4Mar2007.)

⊢ 𝐴 ∈ V & ⊢ (𝜑 → 𝑥 ∈ 𝐴)
& ⊢ {𝑦 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥𝜑} ∈ V 

Theorem  oprabexd 6032* 
Existence of an operator abstraction. (Contributed by Jeff Madsen,
2Sep2009.)

⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑧𝜓)
& ⊢ (𝜑 → 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) 

Theorem  oprabex 6033* 
Existence of an operation class abstraction. (Contributed by NM,
19Oct2004.)

⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃*𝑧𝜑)
& ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⇒ ⊢ 𝐹 ∈ V 

Theorem  oprabex3 6034* 
Existence of an operation class abstraction (special case).
(Contributed by NM, 19Oct2004.)

⊢ 𝐻 ∈ V & ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))} ⇒ ⊢ 𝐹 ∈ V 

Theorem  oprabrexex2 6035* 
Existence of an existentially restricted operation abstraction.
(Contributed by Jeff Madsen, 11Jun2010.)

⊢ 𝐴 ∈ V & ⊢
{⟨⟨𝑥,
𝑦⟩, 𝑧⟩ ∣ 𝜑} ∈ V ⇒ ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑤 ∈ 𝐴 𝜑} ∈ V 

Theorem  ab2rexex 6036* 
Existence of a class abstraction of existentially restricted sets.
Variables 𝑥 and 𝑦 are normally
freevariable parameters in the
class expression substituted for 𝐶, which can be thought of as
𝐶(𝑥, 𝑦). See comments for abrexex 6022. (Contributed by NM,
20Sep2011.)

⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} ∈ V 

Theorem  ab2rexex2 6037* 
Existence of an existentially restricted class abstraction. 𝜑
normally has freevariable parameters 𝑥, 𝑦, and 𝑧.
Compare abrexex2 6029. (Contributed by NM, 20Sep2011.)

⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ {𝑧 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} ∈ V 

Theorem  xpexgALT 6038 
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. This
version is proven using Replacement; see
xpexg 4660 for a version that uses the Power Set axiom
instead.
(Contributed by Mario Carneiro, 20May2013.)
(Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) 

Theorem  offval3 6039* 
General value of (𝐹 ∘_{𝑓} 𝑅𝐺) with no assumptions on
functionality
of 𝐹 and 𝐺. (Contributed by Stefan
O'Rear, 24Jan2015.)

⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘_{𝑓} 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) 

Theorem  offres 6040 
Pointwise combination commutes with restriction. (Contributed by Stefan
O'Rear, 24Jan2015.)

⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘_{𝑓} 𝑅𝐺) ↾ 𝐷) = ((𝐹 ↾ 𝐷) ∘_{𝑓} 𝑅(𝐺 ↾ 𝐷))) 

Theorem  ofmres 6041* 
Equivalent expressions for a restriction of the function operation map.
Unlike ∘_{𝑓} 𝑅 which is a proper class, ( ∘_{𝑓} 𝑅 ↾ (𝐴 × 𝐵)) can
be a set by ofmresex 6042, allowing it to be used as a function or
structure argument. By ofmresval 6000, the restricted operation map
values are the same as the original values, allowing theorems for
∘_{𝑓} 𝑅 to be reused. (Contributed by NM,
20Oct2014.)

⊢ ( ∘_{𝑓} 𝑅 ↾ (𝐴 × 𝐵)) = (𝑓 ∈ 𝐴, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘_{𝑓} 𝑅𝑔)) 

Theorem  ofmresex 6042 
Existence of a restriction of the function operation map. (Contributed
by NM, 20Oct2014.)

⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ( ∘_{𝑓} 𝑅 ↾ (𝐴 × 𝐵)) ∈ V) 

2.6.14 First and second members of an ordered
pair


Syntax  c1st 6043 
Extend the definition of a class to include the first member an ordered
pair function.

class 1^{st} 

Syntax  c2nd 6044 
Extend the definition of a class to include the second member an ordered
pair function.

class 2^{nd} 

Definition  df1st 6045 
Define a function that extracts the first member, or abscissa, of an
ordered pair. Theorem op1st 6051 proves that it does this. For example,
(1^{st} ‘⟨ 3 , 4 ⟩) = 3 . Equivalent to Definition 5.13 (i) of
[Monk1] p. 52 (compare op1sta 5027 and op1stb 4406). The notation is the same
as Monk's. (Contributed by NM, 9Oct2004.)

⊢ 1^{st} = (𝑥 ∈ V ↦ ∪ dom {𝑥}) 

Definition  df2nd 6046 
Define a function that extracts the second member, or ordinate, of an
ordered pair. Theorem op2nd 6052 proves that it does this. For example,
(2^{nd} ‘⟨ 3 , 4 ⟩) = 4 . Equivalent to Definition 5.13 (ii)
of [Monk1] p. 52 (compare op2nda 5030 and op2ndb 5029). The notation is the
same as Monk's. (Contributed by NM, 9Oct2004.)

⊢ 2^{nd} = (𝑥 ∈ V ↦ ∪ ran {𝑥}) 

Theorem  1stvalg 6047 
The value of the function that extracts the first member of an ordered
pair. (Contributed by NM, 9Oct2004.) (Revised by Mario Carneiro,
8Sep2013.)

⊢ (𝐴 ∈ V → (1^{st}
‘𝐴) = ∪ dom {𝐴}) 

Theorem  2ndvalg 6048 
The value of the function that extracts the second member of an ordered
pair. (Contributed by NM, 9Oct2004.) (Revised by Mario Carneiro,
8Sep2013.)

⊢ (𝐴 ∈ V → (2^{nd}
‘𝐴) = ∪ ran {𝐴}) 

Theorem  1st0 6049 
The value of the firstmember function at the empty set. (Contributed by
NM, 23Apr2007.)

⊢ (1^{st} ‘∅) =
∅ 

Theorem  2nd0 6050 
The value of the secondmember function at the empty set. (Contributed by
NM, 23Apr2007.)

⊢ (2^{nd} ‘∅) =
∅ 

Theorem  op1st 6051 
Extract the first member of an ordered pair. (Contributed by NM,
5Oct2004.)

⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (1^{st}
‘⟨𝐴, 𝐵⟩) = 𝐴 

Theorem  op2nd 6052 
Extract the second member of an ordered pair. (Contributed by NM,
5Oct2004.)

⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (2^{nd}
‘⟨𝐴, 𝐵⟩) = 𝐵 

Theorem  op1std 6053 
Extract the first member of an ordered pair. (Contributed by Mario
Carneiro, 31Aug2015.)

⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1^{st} ‘𝐶) = 𝐴) 

Theorem  op2ndd 6054 
Extract the second member of an ordered pair. (Contributed by Mario
Carneiro, 31Aug2015.)

⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (2^{nd} ‘𝐶) = 𝐵) 

Theorem  op1stg 6055 
Extract the first member of an ordered pair. (Contributed by NM,
19Jul2005.)

⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1^{st} ‘⟨𝐴, 𝐵⟩) = 𝐴) 

Theorem  op2ndg 6056 
Extract the second member of an ordered pair. (Contributed by NM,
19Jul2005.)

⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2^{nd} ‘⟨𝐴, 𝐵⟩) = 𝐵) 

Theorem  ot1stg 6057 
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 6057,
ot2ndg 6058, ot3rdgg 6059.) (Contributed by NM, 3Apr2015.) (Revised
by
Mario Carneiro, 2May2015.)

⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (1^{st}
‘(1^{st} ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐴) 

Theorem  ot2ndg 6058 
Extract the second member of an ordered triple. (See ot1stg 6057 comment.)
(Contributed by NM, 3Apr2015.) (Revised by Mario Carneiro,
2May2015.)

⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2^{nd}
‘(1^{st} ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐵) 

Theorem  ot3rdgg 6059 
Extract the third member of an ordered triple. (See ot1stg 6057 comment.)
(Contributed by NM, 3Apr2015.)

⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2^{nd} ‘⟨𝐴, 𝐵, 𝐶⟩) = 𝐶) 

Theorem  1stval2 6060 
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, 18Aug2006.)

⊢ (𝐴 ∈ (V × V) →
(1^{st} ‘𝐴)
= ∩ ∩ 𝐴) 

Theorem  2ndval2 6061 
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, 18Aug2006.)

⊢ (𝐴 ∈ (V × V) →
(2^{nd} ‘𝐴)
= ∩ ∩ ∩ ^{◡}{𝐴}) 

Theorem  fo1st 6062 
The 1^{st} function maps the universe onto the
universe. (Contributed
by NM, 14Oct2004.) (Revised by Mario Carneiro, 8Sep2013.)

⊢ 1^{st} :V–onto→V 

Theorem  fo2nd 6063 
The 2^{nd} function maps the universe onto the
universe. (Contributed
by NM, 14Oct2004.) (Revised by Mario Carneiro, 8Sep2013.)

⊢ 2^{nd} :V–onto→V 

Theorem  f1stres 6064 
Mapping of a restriction of the 1^{st} (first
member of an ordered
pair) function. (Contributed by NM, 11Oct2004.) (Revised by Mario
Carneiro, 8Sep2013.)

⊢ (1^{st} ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐴 

Theorem  f2ndres 6065 
Mapping of a restriction of the 2^{nd} (second
member of an ordered
pair) function. (Contributed by NM, 7Aug2006.) (Revised by Mario
Carneiro, 8Sep2013.)

⊢ (2^{nd} ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐵 

Theorem  fo1stresm 6066* 
Onto mapping of a restriction of the 1^{st}
(first member of an ordered
pair) function. (Contributed by Jim Kingdon, 24Jan2019.)

⊢ (∃𝑦 𝑦 ∈ 𝐵 → (1^{st} ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)–onto→𝐴) 

Theorem  fo2ndresm 6067* 
Onto mapping of a restriction of the 2^{nd}
(second member of an
ordered pair) function. (Contributed by Jim Kingdon, 24Jan2019.)

⊢ (∃𝑥 𝑥 ∈ 𝐴 → (2^{nd} ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)–onto→𝐵) 

Theorem  1stcof 6068 
Composition of the first member function with another function.
(Contributed by NM, 12Oct2007.)

⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (1^{st} ∘ 𝐹):𝐴⟶𝐵) 

Theorem  2ndcof 6069 
Composition of the second member function with another function.
(Contributed by FL, 15Oct2012.)

⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (2^{nd} ∘ 𝐹):𝐴⟶𝐶) 

Theorem  xp1st 6070 
Location of the first element of a Cartesian product. (Contributed by
Jeff Madsen, 2Sep2009.)

⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1^{st} ‘𝐴) ∈ 𝐵) 

Theorem  xp2nd 6071 
Location of the second element of a Cartesian product. (Contributed by
Jeff Madsen, 2Sep2009.)

⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2^{nd} ‘𝐴) ∈ 𝐶) 

Theorem  1stexg 6072 
Existence of the first member of a set. (Contributed by Jim Kingdon,
26Jan2019.)

⊢ (𝐴 ∈ 𝑉 → (1^{st} ‘𝐴) ∈ V) 

Theorem  2ndexg 6073 
Existence of the first member of a set. (Contributed by Jim Kingdon,
26Jan2019.)

⊢ (𝐴 ∈ 𝑉 → (2^{nd} ‘𝐴) ∈ V) 

Theorem  elxp6 6074 
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp4 5033. (Contributed by NM, 9Oct2004.)

⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩ ∧ ((1^{st}
‘𝐴) ∈ 𝐵 ∧ (2^{nd}
‘𝐴) ∈ 𝐶))) 

Theorem  elxp7 6075 
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp4 5033. (Contributed by NM, 19Aug2006.)

⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 ∈ (V × V) ∧
((1^{st} ‘𝐴)
∈ 𝐵 ∧
(2^{nd} ‘𝐴)
∈ 𝐶))) 

Theorem  oprssdmm 6076* 
Domain of closure of an operation. (Contributed by Jim Kingdon,
23Oct2023.)

⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ∃𝑣 𝑣 ∈ 𝑢)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)
& ⊢ (𝜑 → Rel 𝐹) ⇒ ⊢ (𝜑 → (𝑆 × 𝑆) ⊆ dom 𝐹) 

Theorem  eqopi 6077 
Equality with an ordered pair. (Contributed by NM, 15Dec2008.)
(Revised by Mario Carneiro, 23Feb2014.)

⊢ ((𝐴 ∈ (𝑉 × 𝑊) ∧ ((1^{st} ‘𝐴) = 𝐵 ∧ (2^{nd} ‘𝐴) = 𝐶)) → 𝐴 = ⟨𝐵, 𝐶⟩) 

Theorem  xp2 6078* 
Representation of cross product based on ordered pair component
functions. (Contributed by NM, 16Sep2006.)

⊢ (𝐴 × 𝐵) = {𝑥 ∈ (V × V) ∣
((1^{st} ‘𝑥)
∈ 𝐴 ∧
(2^{nd} ‘𝑥)
∈ 𝐵)} 

Theorem  unielxp 6079 
The membership relation for a cross product is inherited by union.
(Contributed by NM, 16Sep2006.)

⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∪ 𝐴 ∈ ∪ (𝐵
× 𝐶)) 

Theorem  1st2nd2 6080 
Reconstruction of a member of a cross product in terms of its ordered pair
components. (Contributed by NM, 20Oct2013.)

⊢ (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 = ⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩) 

Theorem  xpopth 6081 
An ordered pair theorem for members of cross products. (Contributed by
NM, 20Jun2007.)

⊢ ((𝐴 ∈ (𝐶 × 𝐷) ∧ 𝐵 ∈ (𝑅 × 𝑆)) → (((1^{st} ‘𝐴) = (1^{st}
‘𝐵) ∧
(2^{nd} ‘𝐴)
= (2^{nd} ‘𝐵)) ↔ 𝐴 = 𝐵)) 

Theorem  eqop 6082 
Two ways to express equality with an ordered pair. (Contributed by NM,
3Sep2007.) (Proof shortened by Mario Carneiro, 26Apr2015.)

⊢ (𝐴 ∈ (𝑉 × 𝑊) → (𝐴 = ⟨𝐵, 𝐶⟩ ↔ ((1^{st} ‘𝐴) = 𝐵 ∧ (2^{nd} ‘𝐴) = 𝐶))) 

Theorem  eqop2 6083 
Two ways to express equality with an ordered pair. (Contributed by NM,
25Feb2014.)

⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈
V ⇒ ⊢ (𝐴 = ⟨𝐵, 𝐶⟩ ↔ (𝐴 ∈ (V × V) ∧
((1^{st} ‘𝐴)
= 𝐵 ∧ (2^{nd}
‘𝐴) = 𝐶))) 

Theorem  op1steq 6084* 
Two ways of expressing that an element is the first member of an ordered
pair. (Contributed by NM, 22Sep2013.) (Revised by Mario Carneiro,
23Feb2014.)

⊢ (𝐴 ∈ (𝑉 × 𝑊) → ((1^{st} ‘𝐴) = 𝐵 ↔ ∃𝑥 𝐴 = ⟨𝐵, 𝑥⟩)) 

Theorem  2nd1st 6085 
Swap the members of an ordered pair. (Contributed by NM, 31Dec2014.)

⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∪ ^{◡}{𝐴} = ⟨(2^{nd} ‘𝐴), (1^{st} ‘𝐴)⟩) 

Theorem  1st2nd 6086 
Reconstruction of a member of a relation in terms of its ordered pair
components. (Contributed by NM, 29Aug2006.)

⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = ⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩) 

Theorem  1stdm 6087 
The first ordered pair component of a member of a relation belongs to the
domain of the relation. (Contributed by NM, 17Sep2006.)

⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → (1^{st} ‘𝐴) ∈ dom 𝑅) 

Theorem  2ndrn 6088 
The second ordered pair component of a member of a relation belongs to the
range of the relation. (Contributed by NM, 17Sep2006.)

⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → (2^{nd} ‘𝐴) ∈ ran 𝑅) 

Theorem  1st2ndbr 6089 
Express an element of a relation as a relationship between first and
second components. (Contributed by Mario Carneiro, 22Jun2016.)

⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → (1^{st} ‘𝐴)𝐵(2^{nd} ‘𝐴)) 

Theorem  releldm2 6090* 
Two ways of expressing membership in the domain of a relation.
(Contributed by NM, 22Sep2013.)

⊢ (Rel 𝐴 → (𝐵 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1^{st} ‘𝑥) = 𝐵)) 

Theorem  reldm 6091* 
An expression for the domain of a relation. (Contributed by NM,
22Sep2013.)

⊢ (Rel 𝐴 → dom 𝐴 = ran (𝑥 ∈ 𝐴 ↦ (1^{st} ‘𝑥))) 

Theorem  sbcopeq1a 6092 
Equality theorem for substitution of a class for an ordered pair (analog
of sbceq1a 2921 that avoids the existential quantifiers of copsexg 4173).
(Contributed by NM, 19Aug2006.) (Revised by Mario Carneiro,
31Aug2015.)

⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ([(1^{st}
‘𝐴) / 𝑥][(2^{nd}
‘𝐴) / 𝑦]𝜑 ↔ 𝜑)) 

Theorem  csbopeq1a 6093 
Equality theorem for substitution of a class 𝐴 for an ordered pair
⟨𝑥, 𝑦⟩ in 𝐵 (analog of csbeq1a 3015). (Contributed by NM,
19Aug2006.) (Revised by Mario Carneiro, 31Aug2015.)

⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ⦋(1^{st}
‘𝐴) / 𝑥⦌⦋(2^{nd}
‘𝐴) / 𝑦⦌𝐵 = 𝐵) 

Theorem  dfopab2 6094* 
A way to define an orderedpair class abstraction without using
existential quantifiers. (Contributed by NM, 18Aug2006.) (Revised by
Mario Carneiro, 31Aug2015.)

⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∈ (V × V) ∣
[(1^{st} ‘𝑧) / 𝑥][(2^{nd} ‘𝑧) / 𝑦]𝜑} 

Theorem  dfoprab3s 6095* 
A way to define an operation class abstraction without using existential
quantifiers. (Contributed by NM, 18Aug2006.) (Revised by Mario
Carneiro, 31Aug2015.)

⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ (V × V) ∧
[(1^{st} ‘𝑤) / 𝑥][(2^{nd} ‘𝑤) / 𝑦]𝜑)} 

Theorem  dfoprab3 6096* 
Operation class abstraction expressed without existential quantifiers.
(Contributed by NM, 16Dec2008.)

⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ (V × V) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} 

Theorem  dfoprab4 6097* 
Operation class abstraction expressed without existential quantifiers.
(Contributed by NM, 3Sep2007.) (Revised by Mario Carneiro,
31Aug2015.)

⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)} 

Theorem  dfoprab4f 6098* 
Operation class abstraction expressed without existential quantifiers.
(Unnecessary distinct variable restrictions were removed by David
Abernethy, 19Jun2012.) (Contributed by NM, 20Dec2008.) (Revised by
Mario Carneiro, 31Aug2015.)

⊢ Ⅎ𝑥𝜑
& ⊢ Ⅎ𝑦𝜑
& ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)} 

Theorem  dfxp3 6099* 
Define the cross product of three classes. Compare dfxp 4552.
(Contributed by FL, 6Nov2013.) (Proof shortened by Mario Carneiro,
3Nov2015.)

⊢ ((𝐴 × 𝐵) × 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)} 

Theorem  elopabi 6100* 
A consequence of membership in an orderedpair class abstraction, using
ordered pair extractors. (Contributed by NM, 29Aug2006.)

⊢ (𝑥 = (1^{st} ‘𝐴) → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = (2^{nd} ‘𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → 𝜒) 