Type  Label  Description 
Statement 

Theorem  opbr1st 5501 
Binary relationship of an ordered pair over 1^{st}.
(Contributed by
SF, 6Feb2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (⟨A, B⟩1^{st} C ↔ A =
C) 

Theorem  opbr2nd 5502 
Binary relationship of an ordered pair over 2^{nd}.
(Contributed by
SF, 6Feb2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (⟨A, B⟩2^{nd} C ↔ B =
C) 

Theorem  dfid4 5503 
Alternate definition of the identity relationship. (Contributed by SF,
11Feb2015.)

⊢ I = ( S ∩
^{◡} S
) 

Theorem  idex 5504 
The identity relationship is a set. (Contributed by SF, 11Feb2015.)

⊢ I ∈
V 

Theorem  1stfo 5505 
1^{st} is a mapping from the universe onto the universe.
(Contributed by SF, 12Feb2015.) (Revised by Scott Fenton,
17Apr2021.)

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

Theorem  2ndfo 5506 
2^{nd} is a mapping from the universe onto the universe.
(Contributed by SF, 12Feb2015.) (Revised by Scott Fenton,
17Apr2021.)

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

Theorem  dfdm4 5507 
Alternate definition of domain. (Contributed by SF, 23Feb2015.)

⊢ dom A =
(1^{st} “ A) 

Theorem  dfrn5 5508 
Alternate definition of range. (Contributed by SF, 23Feb2015.)

⊢ ran A =
(2^{nd} “ A) 

Theorem  brswap 5509* 
Binary relationship of Swap .
(Contributed by SF, 23Feb2015.)

⊢ (A Swap B ↔
∃x∃y(A = ⟨x, y⟩ ∧ B = ⟨y, x⟩)) 

Theorem  cnvswap 5510 
The converse of Swap is Swap . (Contributed by SF,
23Feb2015.)

⊢ ^{◡} Swap = Swap


Theorem  swapf1o 5511 
Swap is a bijection over the
universe. (Contributed by SF,
23Feb2015.) (Revised by Scott Fenton, 17Apr2021.)

⊢ Swap
:V–11onto→V 

Theorem  swapres 5512 
Bijection law for restrictions of Swap
. (Contributed by SF,
23Feb2015.) (Modified by Scott Fenton, 17Apr2021.)

⊢ ( Swap ↾ A):A–11onto→^{◡}A 

Theorem  xpnedisj 5513 
Cross products with nonequal singletons are disjoint. (Contributed by
SF, 23Feb2015.)

⊢ C ∈ V
& ⊢ C ≠
D ⇒ ⊢ ((A ×
{C}) ∩ (B × {D}))
= ∅ 

Theorem  opfv1st 5514 
The value of the 1^{st} function on an ordered pair.
(Contributed by
SF, 23Feb2015.)

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

Theorem  opfv2nd 5515 
The value of the 2^{nd} function on an ordered pair.
(Contributed by
SF, 23Feb2015.)

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

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

⊢ (A ∈ (B ×
C) → A = ⟨(1^{st} ‘A), (2^{nd} ‘A)⟩) 

Theorem  fununiq 5517 
Implicational form of part of the definition of a function.
(Contributed by SF, 24Feb2015.)

⊢ ((Fun F
∧ AFB ∧ AFC) → B =
C) 

Theorem  cnvsi 5518 
Calculate the converse of a singleton image. (Contributed by SF,
26Feb2015.)

⊢ ^{◡} SI R = SI ^{◡}R 

Theorem  dmsi 5519 
Calculate the domain of a singleton image. Theorem X.4.29.I of [Rosser]
p. 301. (Contributed by SF, 26Feb2015.)

⊢ dom SI R = ℘_{1}dom R 

Theorem  funsi 5520 
The singleton image of a function is a function. (Contributed by SF,
26Feb2015.)

⊢ (Fun F
→ Fun SI F) 

Theorem  rnsi 5521 
Calculate the range of a singleton image. Theorem X.4.29.II of [Rosser]
p. 302. (Contributed by SF, 26Feb2015.)

⊢ ran SI R = ℘_{1}ran R 

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

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (C = ⟨A, B⟩ →
(1^{st} ‘C) = A) 

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

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (C = ⟨A, B⟩ →
(2^{nd} ‘C) = B) 

Theorem  dmep 5524 
The domain of the epsilon relationship. (Contributed by Scott Fenton,
20Apr2021.)

⊢ dom E = V 

2.3.8 Operations


Syntax  co 5525 
Extend class notation to include the value of an operation F for two
arguments A and B. Note that the syntax is simply
three class
symbols in a row surrounded by parentheses. Since operation values are
the only possible class expressions consisting of three class expressions
in a row surrounded by parentheses, the syntax is unambiguous.

class
(AFB) 

Definition  dfov 5526 
Define the value of an operation. Definition of operation value in
[Enderton] p. 79. Note that the syntax
is simply three class expressions
in a row bracketed by parentheses. There are no restrictions of any kind
on what those class expressions may be, although only certain kinds of
class expressions  a binary operation F and its arguments A and
B will be useful for
proving meaningful theorems. This definition
is welldefined, although not very meaningful, when classes A and/or
B are proper classes
(i.e. are not sets). On the other hand, we often
find uses for this definition when F is a proper class. F is
normally equal to a class of nested ordered pairs of the form defined by
dfoprab 5528. (Contributed by SF, 5Jan2015.)

⊢ (AFB) = (F ‘⟨A, B⟩) 

Syntax  coprab 5527 
Extend class notation to include class abstraction (class builder) of
nested ordered pairs.

class
{⟨⟨x, y⟩, z⟩ ∣ φ} 

Definition  dfoprab 5528* 
Define the class abstraction (class builder) of a collection of nested
ordered pairs (for use in defining operations). This is a special case
of Definition 4.16 of [TakeutiZaring] p. 14. Normally x, y,
and z are distinct,
although the definition doesn't strictly require
it. See dfov 5526 for the value of an operation. The brace
notation is
called "class abstraction" by Quine; it is also called a
"class builder"
in the literature. The value of the most common operation class builder
is given by ov2 in set.mm. (Contributed by SF, 5Jan2015.)

⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} =
{w ∣
∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)} 

Theorem  oveq 5529 
Equality theorem for operation value. (Contributed by set.mm
contributors, 28Feb1995.)

⊢ (F =
G → (AFB) = (AGB)) 

Theorem  oveq1 5530 
Equality theorem for operation value. (Contributed by set.mm
contributors, 28Feb1995.)

⊢ (A =
B → (AFC) = (BFC)) 

Theorem  oveq2 5531 
Equality theorem for operation value. (Contributed by set.mm
contributors, 28Feb1995.)

⊢ (A =
B → (CFA) = (CFB)) 

Theorem  oveq12 5532 
Equality theorem for operation value. (Contributed by set.mm
contributors, 16Jul1995.)

⊢ ((A =
B ∧
C = D)
→ (AFC) = (BFD)) 

Theorem  oveq1i 5533 
Equality inference for operation value. (Contributed by set.mm
contributors, 28Feb1995.)

⊢ A =
B ⇒ ⊢ (AFC) = (BFC) 

Theorem  oveq2i 5534 
Equality inference for operation value. (Contributed by set.mm
contributors, 28Feb1995.)

⊢ A =
B ⇒ ⊢ (CFA) = (CFB) 

Theorem  oveq12i 5535 
Equality inference for operation value. (The proof was shortened by
Andrew Salmon, 22Oct2011.) (Contributed by set.mm contributors,
28Feb1995.) (Revised by set.mm contributors, 22Oct2011.)

⊢ A =
B
& ⊢ C =
D ⇒ ⊢ (AFC) = (BFD) 

Theorem  oveqi 5536 
Equality inference for operation value. (Contributed by set.mm
contributors, 24Nov2007.)

⊢ A =
B ⇒ ⊢ (CAD) = (CBD) 

Theorem  oveq1d 5537 
Equality deduction for operation value. (Contributed by set.mm
contributors, 13Mar1995.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (AFC) = (BFC)) 

Theorem  oveq2d 5538 
Equality deduction for operation value. (Contributed by set.mm
contributors, 13Mar1995.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (CFA) = (CFB)) 

Theorem  oveqd 5539 
Equality deduction for operation value. (Contributed by set.mm
contributors, 9Sep2006.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (CAD) = (CBD)) 

Theorem  oveq12d 5540 
Equality deduction for operation value. (The proof was shortened by
Andrew Salmon, 22Oct2011.) (Contributed by set.mm contributors,
13Mar1995.) (Revised by set.mm contributors, 22Oct2011.)

⊢ (φ
→ A = B)
& ⊢ (φ
→ C = D) ⇒ ⊢ (φ
→ (AFC) = (BFD)) 

Theorem  oveqan12d 5541 
Equality deduction for operation value. (Contributed by set.mm
contributors, 10Aug1995.)

⊢ (φ
→ A = B)
& ⊢ (ψ
→ C = D) ⇒ ⊢ ((φ
∧ ψ)
→ (AFC) = (BFD)) 

Theorem  oveqan12rd 5542 
Equality deduction for operation value. (Contributed by set.mm
contributors, 10Aug1995.)

⊢ (φ
→ A = B)
& ⊢ (ψ
→ C = D) ⇒ ⊢ ((ψ
∧ φ)
→ (AFC) = (BFD)) 

Theorem  oveq123d 5543 
Equality deduction for operation value. (Contributed by FL,
22Dec2008.)

⊢ (φ
→ F = G)
& ⊢ (φ
→ A = B)
& ⊢ (φ
→ C = D) ⇒ ⊢ (φ
→ (AFC) = (BGD)) 

Theorem  nfovd 5544 
Deduction version of boundvariable hypothesis builder nfov 5545.
(Contributed by NM, 13Dec2005.) (Proof shortened by Andrew Salmon,
22Oct2011.)

⊢ (φ
→ ℲxA)
& ⊢ (φ
→ ℲxF)
& ⊢ (φ
→ ℲxB) ⇒ ⊢ (φ
→ Ⅎx(AFB)) 

Theorem  nfov 5545 
Boundvariable hypothesis builder for operation value. (Contributed by
NM, 4May2004.)

⊢ ℲxA & ⊢ ℲxF & ⊢ ℲxB ⇒ ⊢ Ⅎx(AFB) 

Theorem  nfoprab1 5546 
The abstraction variables in an operation class abstraction are not
free. (Contributed by NM, 25Apr1995.) (Revised by David Abernethy,
19Jun2012.)

⊢ Ⅎx{⟨⟨x, y⟩, z⟩ ∣ φ} 

Theorem  nfoprab2 5547 
The abstraction variables in an operation class abstraction are not
free. (Contributed by NM, 25Apr1995.) (Revised by David Abernethy,
30Jul2012.)

⊢ Ⅎy{⟨⟨x, y⟩, z⟩ ∣ φ} 

Theorem  nfoprab3 5548 
The abstraction variables in an operation class abstraction are not
free. (Contributed by NM, 22Aug2013.)

⊢ Ⅎz{⟨⟨x, y⟩, z⟩ ∣ φ} 

Theorem  nfoprab 5549* 
Boundvariable hypothesis builder for an operation class abstraction.
(Contributed by NM, 22Aug2013.)

⊢ Ⅎwφ ⇒ ⊢ Ⅎw{⟨⟨x, y⟩, z⟩ ∣ φ} 

Theorem  oprabid 5550 
The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
(Contributed by Mario Carneiro, 20Mar2013.)

⊢ (⟨⟨x, y⟩, z⟩ ∈ {⟨⟨x, y⟩, z⟩ ∣ φ}
↔ φ) 

Theorem  ovex 5551 
The result of an operation is a set. (Contributed by set.mm contributors,
13Mar1995.)

⊢ (AFB) ∈ V 

Theorem  csbovg 5552 
Move class substitution in and out of an operation. (Contributed by NM,
12Nov2005.) (Proof shortened by Mario Carneiro, 5Dec2016.)

⊢ (A ∈ D →
[A / x](BFC) = ([A
/ x]B[A /
x]F[A /
x]C)) 

Theorem  csbov12g 5553* 
Move class substitution in and out of an operation. (Contributed by NM,
12Nov2005.)

⊢ (A ∈ D →
[A / x](BFC) = ([A
/ x]BF[A /
x]C)) 

Theorem  csbov1g 5554* 
Move class substitution in and out of an operation. (Contributed by NM,
12Nov2005.)

⊢ (A ∈ D →
[A / x](BFC) = ([A
/ x]BFC)) 

Theorem  csbov2g 5555* 
Move class substitution in and out of an operation. (Contributed by NM,
12Nov2005.)

⊢ (A ∈ D →
[A / x](BFC) = (BF[A /
x]C)) 

Theorem  rspceov 5556* 
A frequently used special case of rspc2ev 2963 for operation values.
(Contributed by set.mm contributors, 21Mar2007.)

⊢ ((C ∈ A ∧ D ∈ B ∧ S = (CFD)) → ∃x ∈ A ∃y ∈ B S = (xFy)) 

Theorem  fnopovb 5557 
Equivalence of operation value and ordered triple membership, analogous to
fnopfvb 5359. (Contributed by set.mm contributors,
17Dec2008.)

⊢ ((F Fn
(A × B) ∧ C ∈ A ∧ D ∈ B) → ((CFD) = R ↔
⟨⟨C, D⟩, R⟩ ∈ F)) 

Theorem  dfoprab2 5558* 
Class abstraction for operations in terms of class abstraction of
ordered pairs. (Contributed by set.mm contributors, 12Mar1995.)

⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} =
{⟨w,
z⟩ ∣ ∃x∃y(w = ⟨x, y⟩ ∧ φ)} 

Theorem  hboprab1 5559* 
The abstraction variables in an operation class abstraction are not
free. (Unnecessary distinct variable restrictions were removed by David
Abernethy, 19Jun2012.) (Contributed by set.mm contributors,
25Apr1995.) (Revised by set.mm contributors, 24Jul2012.)

⊢ (w ∈ {⟨⟨x, y⟩, z⟩ ∣ φ}
→ ∀x w ∈ {⟨⟨x, y⟩, z⟩ ∣ φ}) 

Theorem  hboprab2 5560* 
The abstraction variables in an operation class abstraction are not
free. (Unnecessary distinct variable restrictions were removed by David
Abernethy, 30Jul2012.) (Contributed by set.mm contributors,
25Apr1995.) (Revised by set.mm contributors, 31Jul2012.)

⊢ (w ∈ {⟨⟨x, y⟩, z⟩ ∣ φ}
→ ∀y w ∈ {⟨⟨x, y⟩, z⟩ ∣ φ}) 

Theorem  hboprab3 5561* 
The abstraction variables in an operation class abstraction are not
free. (Contributed by set.mm contributors, 22Aug2013.)

⊢ (w ∈ {⟨⟨x, y⟩, z⟩ ∣ φ}
→ ∀z w ∈ {⟨⟨x, y⟩, z⟩ ∣ φ}) 

Theorem  hboprab 5562* 
Boundvariable hypothesis builder for an operation class abstraction.
(Contributed by set.mm contributors, 22Aug2013.)

⊢ (φ
→ ∀wφ) ⇒ ⊢ (u ∈ {⟨⟨x, y⟩, z⟩ ∣ φ}
→ ∀w u ∈ {⟨⟨x, y⟩, z⟩ ∣ φ}) 

Theorem  oprabbid 5563* 
Equivalent wff's yield equal operation class abstractions (deduction
rule). (Contributed by NM, 21Feb2004.) (Revised by Mario Carneiro,
24Jun2014.)

⊢ Ⅎxφ
& ⊢ Ⅎyφ
& ⊢ Ⅎzφ
& ⊢ (φ
→ (ψ ↔ χ)) ⇒ ⊢ (φ
→ {⟨⟨x, y⟩, z⟩ ∣ ψ} =
{⟨⟨x, y⟩, z⟩ ∣ χ}) 

Theorem  oprabbidv 5564* 
Equivalent wff's yield equal operation class abstractions (deduction
rule). (Contributed by NM, 21Feb2004.)

⊢ (φ
→ (ψ ↔ χ)) ⇒ ⊢ (φ
→ {⟨⟨x, y⟩, z⟩ ∣ ψ} =
{⟨⟨x, y⟩, z⟩ ∣ χ}) 

Theorem  oprabbii 5565* 
Equivalent wff's yield equal operation class abstractions. (Unnecessary
distinct variable restrictions were removed by David Abernethy,
19Jun2012.) (Contributed by set.mm contributors, 28May1995.)
(Revised by set.mm contributors, 24Jul2012.)

⊢ (φ
↔ ψ)
⇒ ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, z⟩ ∣ ψ} 

Theorem  oprab4 5566* 
Two ways to state the domain of an operation. (Contributed by FL,
24Jan2010.)

⊢ {⟨⟨x, y⟩, z⟩ ∣ (⟨x, y⟩ ∈ (A × B)
∧ φ)}
= {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} 

Theorem  cbvoprab1 5567* 
Rule used to change first bound variable in an operation abstraction,
using implicit substitution. (Contributed by NM, 20Dec2008.)
(Revised by Mario Carneiro, 5Dec2016.)

⊢ Ⅎwφ
& ⊢ Ⅎxψ
& ⊢ (x =
w → (φ ↔ ψ)) ⇒ ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} =
{⟨⟨w, y⟩, z⟩ ∣ ψ} 

Theorem  cbvoprab2 5568* 
Change the second bound variable in an operation abstraction.
(Contributed by Jeff Madsen, 11Jun2010.) (Revised by Mario Carneiro,
11Dec2016.)

⊢ Ⅎwφ
& ⊢ Ⅎyψ
& ⊢ (y =
w → (φ ↔ ψ)) ⇒ ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} =
{⟨⟨x, w⟩, z⟩ ∣ ψ} 

Theorem  cbvoprab12 5569* 
Rule used to change first two bound variables in an operation
abstraction, using implicit substitution. (Contributed by NM,
21Feb2004.) (Proof shortened by Andrew Salmon, 22Oct2011.)

⊢ Ⅎwφ
& ⊢ Ⅎvφ
& ⊢ Ⅎxψ
& ⊢ Ⅎyψ
& ⊢ ((x =
w ∧
y = v)
→ (φ ↔ ψ)) ⇒ ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} =
{⟨⟨w, v⟩, z⟩ ∣ ψ} 

Theorem  cbvoprab12v 5570* 
Rule used to change first two bound variables in an operation
abstraction, using implicit substitution. (Contributed by set.mm
contributors, 8Oct2004.)

⊢ ((x =
w ∧
y = v)
→ (φ ↔ ψ)) ⇒ ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} =
{⟨⟨w, v⟩, z⟩ ∣ ψ} 

Theorem  cbvoprab3 5571* 
Rule used to change the third bound variable in an operation
abstraction, using implicit substitution. (Contributed by NM,
22Aug2013.)

⊢ Ⅎwφ
& ⊢ Ⅎzψ
& ⊢ (z =
w → (φ ↔ ψ)) ⇒ ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} =
{⟨⟨x, y⟩, w⟩ ∣ ψ} 

Theorem  cbvoprab3v 5572* 
Rule used to change the third bound variable in an operation
abstraction, using implicit substitution. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 19Jun2012.)
(Contributed by set.mm contributors, 8Oct2004.) (Revised by set.mm
contributors, 24Jul2012.)

⊢ (z =
w → (φ ↔ ψ)) ⇒ ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} =
{⟨⟨x, y⟩, w⟩ ∣ ψ} 

Theorem  elimdelov 5573 
Eliminate a hypothesis which is a predicate expressing membership in the
result of an operator (deduction version). (Contributed by Paul
Chapman, 25Mar2008.)

⊢ (φ
→ C ∈ (AFB))
& ⊢ Z ∈ (XFY) ⇒ ⊢ if(φ,
C, Z)
∈ ( if(φ, A,
X)F
if(φ, B, Y)) 

Theorem  dmoprab 5574* 
The domain of an operation class abstraction. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 19Jun2012.)
(Contributed by set.mm contributors, 17Mar1995.) (Revised by set.mm
contributors, 24Jul2012.)

⊢ dom {⟨⟨x, y⟩, z⟩ ∣ φ} =
{⟨x,
y⟩ ∣ ∃zφ} 

Theorem  dmoprabss 5575* 
The domain of an operation class abstraction. (Contributed by set.mm
contributors, 24Aug1995.)

⊢ dom {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} ⊆ (A ×
B) 

Theorem  rnoprab 5576* 
The range of an operation class abstraction. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 19Apr2013.)
(Contributed by set.mm contributors, 30Aug2004.) (Revised by set.mm
contributors, 19Apr2013.)

⊢ ran {⟨⟨x, y⟩, z⟩ ∣ φ} =
{z ∣
∃x∃yφ} 

Theorem  rnoprab2 5577* 
The range of a restricted operation class abstraction. (Contributed by
Scott Fenton, 21Mar2012.)

⊢ ran {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} =
{z ∣
∃x
∈ A
∃y
∈ B
φ} 

Theorem  eloprabga 5578* 
The law of concretion for operation class abstraction. Compare
elopab 4696. (Contributed by set.mm contributors,
17Dec2013.) (Revised
by David Abernethy, 18Jun2012.) Removed unnecessary distinct variable
requirements. (Revised by Mario Carneiro, 19Dec2013.)

⊢ ((x =
A ∧
y = B
∧ z =
C) → (φ ↔ ψ)) ⇒ ⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) →
(⟨⟨A, B⟩, C⟩ ∈ {⟨⟨x, y⟩, z⟩ ∣ φ}
↔ ψ)) 

Theorem  eloprabg 5579* 
The law of concretion for operation class abstraction. Compare
elopab 4696. (Contributed by set.mm contributors,
14Sep1999.) (Revised
by David Abernethy, 19Jun2012.) Removed unnecessary distinct variable
requirements. (Revised by set.mm contributors, 19Dec2013.)

⊢ (x =
A → (φ ↔ ψ))
& ⊢ (y =
B → (ψ ↔ χ))
& ⊢ (z =
C → (χ ↔ θ)) ⇒ ⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) →
(⟨⟨A, B⟩, C⟩ ∈ {⟨⟨x, y⟩, z⟩ ∣ φ}
↔ θ)) 

Theorem  ssoprab2i 5580* 
Inference of operation class abstraction subclass from implication.
(Unnecessary distinct variable restrictions were removed by David
Abernethy, 19Jun2012.) (Contributed by set.mm contributors,
11Nov1995.) (Revised by set.mm contributors, 24Jul2012.)

⊢ (φ
→ ψ)
⇒ ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} ⊆
{⟨⟨x, y⟩, z⟩ ∣ ψ} 

Theorem  resoprab 5581* 
Restriction of an operation class abstraction. (Contributed by set.mm
contributors, 10Feb2007.)

⊢ ({⟨⟨x, y⟩, z⟩ ∣ φ}
↾ (A
× B)) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} 

Theorem  resoprab2 5582* 
Restriction of an operator abstraction. (Contributed by Jeff Madsen,
2Sep2009.)

⊢ ((C ⊆ A ∧ D ⊆ B) →
({⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} ↾ (C ×
D)) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ C ∧ y ∈ D) ∧ φ)}) 

Theorem  funoprabg 5583* 
"At most one" is a sufficient condition for an operation class
abstraction to be a function. (Contributed by set.mm contributors,
28Aug2007.)

⊢ (∀x∀y∃*zφ →
Fun {⟨⟨x, y⟩, z⟩ ∣ φ}) 

Theorem  funoprab 5584* 
"At most one" is a sufficient condition for an operation class
abstraction to be a function. (Contributed by set.mm contributors,
17Mar1995.)

⊢ ∃*zφ ⇒ ⊢ Fun {⟨⟨x, y⟩, z⟩ ∣ φ} 

Theorem  fnoprabg 5585* 
Functionality and domain of an operation class abstraction.
(Contributed by set.mm contributors, 28Aug2007.)

⊢ (∀x∀y(φ →
∃!zψ) →
{⟨⟨x, y⟩, z⟩ ∣ (φ
∧ ψ)}
Fn {⟨x,
y⟩ ∣ φ}) 

Theorem  fnoprab 5586* 
Functionality and domain of an operation class abstraction.
(Contributed by set.mm contributors, 15May1995.)

⊢ (φ
→ ∃!zψ) ⇒ ⊢ {⟨⟨x, y⟩, z⟩ ∣ (φ
∧ ψ)}
Fn {⟨x,
y⟩ ∣ φ} 

Theorem  ffnov 5587* 
An operation maps to a class to which all values belong. (Contributed
by set.mm contributors, 7Feb2004.)

⊢ (F:(A ×
B)–→C ↔ (F Fn
(A × B) ∧ ∀x ∈ A ∀y ∈ B (xFy) ∈ C)) 

Theorem  fovcl 5588 
Closure law for an operation. (Contributed by set.mm contributors,
19Apr2007.)

⊢ F:(R × S)–→C ⇒ ⊢ ((A ∈ R ∧ B ∈ S) →
(AFB) ∈ C) 

Theorem  eqfnov 5589* 
Equality of two operations is determined by their values. (Contributed
by set.mm contributors, 1Sep2005.)

⊢ ((F Fn
(A × B) ∧ G Fn (C ×
D)) → (F = G ↔
((A × B) = (C ×
D) ∧
∀x
∈ A
∀y
∈ B
(xFy) = (xGy)))) 

Theorem  eqfnov2 5590* 
Two operators with the same domain are equal iff their values at each
point in the domain are equal. (Contributed by Jeff Madsen,
7Jun2010.)

⊢ ((F Fn
(A × B) ∧ G Fn (A ×
B)) → (F = G ↔
∀x
∈ A
∀y
∈ B
(xFy) = (xGy))) 

Theorem  fnov 5591* 
Representation of an operation class abstraction in terms of its
values. (Contributed by set.mm contributors, 7Feb2004.)

⊢ (F Fn
(A × B) ↔ F =
{⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = (xFy))}) 

Theorem  fov 5592* 
Representation of an operation class abstraction in terms of its
values. (Contributed by set.mm contributors, 7Feb2004.)

⊢ (F:(A ×
B)–→C ↔ (F =
{⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = (xFy))} ∧ ∀x ∈ A ∀y ∈ B (xFy) ∈ C)) 

Theorem  ovidig 5593* 
The value of an operation class abstraction. Compare ovidi 5594. The
condition (x ∈ R ∧ y ∈ S) is
been removed. (Contributed by
Mario Carneiro, 29Dec2014.)

⊢ ∃*zφ
& ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ φ} ⇒ ⊢ (φ
→ (xFy) = z) 

Theorem  ovidi 5594* 
The value of an operation class abstraction (weak version).
(Contributed by Mario Carneiro, 29Dec2014.)

⊢ ((x ∈ R ∧ y ∈ S) →
∃*zφ)
& ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ R ∧ y ∈ S) ∧ φ)} ⇒ ⊢ ((x ∈ R ∧ y ∈ S) →
(φ → (xFy) = z)) 

Theorem  ov 5595* 
The value of an operation class abstraction. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 19Jun2012.)
(Contributed by set.mm contributors, 16May1995.) (Revised by set.mm
contributors, 24Jul2012.)

⊢ C ∈ V
& ⊢ (x =
A → (φ ↔ ψ))
& ⊢ (y =
B → (ψ ↔ χ))
& ⊢ (z =
C → (χ ↔ θ))
& ⊢ ((x ∈ R ∧ y ∈ S) →
∃!zφ)
& ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ R ∧ y ∈ S) ∧ φ)} ⇒ ⊢ ((A ∈ R ∧ B ∈ S) →
((AFB) = C ↔ θ)) 

Theorem  ovigg 5596* 
The value of an operation class abstraction. Compare ovig 5597.
The
condition (x ∈ R ∧ y ∈ S) is
been removed. (Contributed by FL,
24Mar2007.)

⊢ ((x =
A ∧
y = B
∧ z =
C) → (φ ↔ ψ))
& ⊢ ∃*zφ
& ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ φ} ⇒ ⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) →
(ψ → (AFB) = C)) 

Theorem  ovig 5597* 
The value of an operation class abstraction (weak version).
(Contributed by set.mm contributors, 14Sep1999.) (Unnecessary
distinct variable restrictions were removed by David Abernethy,
19Jun2012.) (Revised by Mario Carneiro, 19Dec2013.)

⊢ ((x =
A ∧
y = B
∧ z =
C) → (φ ↔ ψ))
& ⊢ ((x ∈ R ∧ y ∈ S) →
∃*zφ)
& ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ R ∧ y ∈ S) ∧ φ)} ⇒ ⊢ ((A ∈ R ∧ B ∈ S ∧ C ∈ D) →
(ψ → (AFB) = C)) 

Theorem  ov2ag 5598* 
The value of an operation class abstraction. Special case.
(Contributed by Mario Carneiro, 19Dec2013.)

⊢ ((x =
A ∧
y = B)
→ R = S)
& ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ C ∧ y ∈ D) ∧ z = R)} ⇒ ⊢ ((A ∈ C ∧ B ∈ D ∧ S ∈ H) →
(AFB) = S) 

Theorem  ov3 5599* 
The value of an operation class abstraction. Special case.
(Contributed by NM, 28May1995.) (Revised by Mario Carneiro,
29Dec2014.)

⊢ S ∈ V
& ⊢ (((w =
A ∧
v = B)
∧ (u =
C ∧
f = D)) → R =
S)
& ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ (H × H)
∧ y ∈ (H ×
H)) ∧
∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = R))} ⇒ ⊢ (((A ∈ H ∧ B ∈ H) ∧ (C ∈ H ∧ D ∈ H)) →
(⟨A,
B⟩F⟨C, D⟩) = S) 

Theorem  ov6g 5600* 
The value of an operation class abstraction. Special case.
(Contributed by set.mm contributors, 13Nov2006.)

⊢ (⟨x, y⟩ = ⟨A, B⟩ → R =
S)
& ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ (⟨x, y⟩ ∈ C ∧ z = R)} ⇒ ⊢ (((A ∈ G ∧ B ∈ H ∧ ⟨A, B⟩ ∈ C) ∧ S ∈ J) → (AFB) = S) 