Type  Label  Description 
Statement 

Theorem  proj2op 4601 
The second projection operator applied to an ordered pair yields its
second member. Theorem X.2.8 of [Rosser]
p. 283. (Contributed by SF,
3Feb2015.)

⊢ Proj2 ⟨A, B⟩ = B 

Theorem  opth 4602 
The ordered pair theorem. Two ordered pairs are equal iff their
components are equal. (Contributed by SF, 2Jan2015.)

⊢ (⟨A, B⟩ = ⟨C, D⟩ ↔ (A =
C ∧
B = D)) 

Theorem  opexb 4603 
An ordered pair is a set iff its components are sets. (Contributed by SF,
2Jan2015.)

⊢ (⟨A, B⟩ ∈ V ↔
(A ∈ V
∧ B ∈ V)) 

Theorem  nfop 4604 
Boundvariable hypothesis builder for ordered pairs. (Contributed by
SF, 2Jan2015.)

⊢ ℲxA & ⊢ ℲxB ⇒ ⊢ Ⅎx⟨A, B⟩ 

Theorem  nfopd 4605 
Deduction version of boundvariable hypothesis builder nfop 4604.
(Contributed by SF, 2Jan2015.)

⊢ (φ
→ ℲxA)
& ⊢ (φ
→ ℲxB) ⇒ ⊢ (φ
→ Ⅎx⟨A, B⟩) 

Theorem  eqvinop 4606* 
A variable introduction law for ordered pairs. Analog of Lemma 15 of
[Monk2] p. 109. (Contributed by NM,
28May1995.)

⊢ B ∈ V
& ⊢ C ∈ V ⇒ ⊢ (A = ⟨B, C⟩ ↔ ∃x∃y(A = ⟨x, y⟩ ∧ ⟨x, y⟩ = ⟨B, C⟩)) 

Theorem  copsexg 4607* 
Substitution of class A for
ordered pair ⟨x, y⟩.
(Contributed by NM, 27Dec1996.) (Revised by Andrew Salmon,
25Jul2011.)

⊢ (A = ⟨x, y⟩ → (φ ↔ ∃x∃y(A = ⟨x, y⟩ ∧ φ))) 

Theorem  copsex2t 4608* 
Closed theorem form of copsex2g 4609. (Contributed by NM,
17Feb2013.)

⊢ ((∀x∀y((x = A ∧ y = B) →
(φ ↔ ψ)) ∧
(A ∈
V ∧
B ∈
W)) → (∃x∃y(⟨A, B⟩ = ⟨x, y⟩ ∧ φ) ↔
ψ)) 

Theorem  copsex2g 4609* 
Implicit substitution inference for ordered pairs. (Contributed by NM,
28May1995.)

⊢ ((x =
A ∧
y = B)
→ (φ ↔ ψ)) ⇒ ⊢ ((A ∈ V ∧ B ∈ W) →
(∃x∃y(⟨A, B⟩ = ⟨x, y⟩ ∧ φ) ↔ ψ)) 

Theorem  copsex4g 4610* 
An implicit substitution inference for 2 ordered pairs. (Contributed by
NM, 5Aug1995.)

⊢ (((x =
A ∧
y = B)
∧ (z =
C ∧
w = D)) → (φ ↔ ψ)) ⇒ ⊢ (((A ∈ R ∧ B ∈ S) ∧ (C ∈ R ∧ D ∈ S)) →
(∃x∃y∃z∃w((⟨A, B⟩ = ⟨x, y⟩ ∧ ⟨C, D⟩ = ⟨z, w⟩) ∧ φ) ↔
ψ)) 

Theorem  eqop 4611* 
Express equality to an ordered pair. (Contributed by SF,
6Jan2015.)

⊢ (A = ⟨B, C⟩ ↔ ∀z(z ∈ A ↔ (∃t ∈ B z = Phi t ∨ ∃t ∈ C z = ( Phi t ∪ {0_{c}})))) 

Theorem  mosubopt 4612* 
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28Aug2007.)

⊢ (∀y∀z∃*xφ →
∃*x∃y∃z(A = ⟨y, z⟩ ∧ φ)) 

Theorem  mosubop 4613* 
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28May1995.)

⊢ ∃*xφ ⇒ ⊢ ∃*x∃y∃z(A = ⟨y, z⟩ ∧ φ) 

Theorem  phiun 4614 
The phi operation distributes over union. (Contributed by SF,
20Feb2015.)

⊢ Phi (A ∪ B) =
( Phi A ∪
Phi B) 

Theorem  phidisjnn 4615 
The phi operation applied to a set disjoint from the naturals has no
effect. (Contributed by SF, 20Feb2015.)

⊢ ((A ∩
Nn ) = ∅
→ Phi A
= A) 

Theorem  phialllem1 4616* 
Lemma for phiall 4618. Any set of numbers without zero is the
Phi of a set. (Contributed by Scott Fenton, 14Apr2021.)

⊢ A ∈ V ⇒ ⊢ ((A ⊆ Nn ∧ ¬ 0_{c} ∈ A) →
∃x
A = Phi
x) 

Theorem  phialllem2 4617* 
Lemma for phiall 4618. Any set without 0_{c} is equal to the Phi
of a set. (Contributed by Scott Fenton, 8Apr2021.)

⊢ A ∈ V ⇒ ⊢ (¬ 0_{c} ∈ A →
∃x
A = Phi
x) 

Theorem  phiall 4618* 
Any set is equal to either the Phi
of another set or to a Phi
with 0_{c} adjoined. (Contributed by Scott
Fenton, 8Apr2021.)

⊢ A ∈ V ⇒ ⊢ ∃x(A = Phi x ∨ A = ( Phi x ∪
{0_{c}})) 

Theorem  opeq 4619 
Any class is equal to an ordered pair. (Contributed by Scott Fenton,
8Apr2021.)

⊢ A = ⟨ Proj1 A, Proj2 A⟩ 

Theorem  opeqexb 4620* 
A class is a set iff it is equal to an ordered pair. (Contributed by
Scott Fenton, 19Apr2021.)

⊢ (A ∈ V ↔ ∃x∃y A = ⟨x, y⟩) 

Theorem  opeqex 4621* 
Any set is equal to some ordered pair. (Contributed by Scott Fenton,
16Apr2021.)

⊢ (A ∈ V →
∃x∃y A = ⟨x, y⟩) 

2.3.2 Orderedpair class abstractions (class
builders)


Syntax  copab 4622 
Extend class notation to include orderedpair class abstraction (class
builder).

class
{⟨x, y⟩ ∣ φ} 

Definition  dfopab 4623* 
Define the class abstraction of a collection of ordered pairs.
Definition 3.3 of [Monk1] p. 34. Usually
x and y are distinct,
although the definition doesn't strictly require it (see dfid2 4769 for a
case where they are not distinct). The brace notation is called
"class
abstraction" by Quine; it is also (more commonly) called a
"class
builder" in the literature. (Contributed by SF, 12Jan2015.)

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

Theorem  opabbid 4624 
Equivalent wff's yield equal orderedpair class abstractions (deduction
rule). (Contributed by NM, 21Feb2004.) (Proof shortened by Andrew
Salmon, 9Jul2011.)

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

Theorem  opabbidv 4625* 
Equivalent wff's yield equal orderedpair class abstractions (deduction
rule). (Contributed by NM, 15May1995.)

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

Theorem  opabbii 4626 
Equivalent wff's yield equal class abstractions. (Contributed by NM,
15May1995.)

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

Theorem  nfopab 4627* 
Boundvariable hypothesis builder for class abstraction. (Contributed
by NM, 1Sep1999.) (Unnecessary distinct variable restrictions were
removed by Andrew Salmon, 11Jul2011.)

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

Theorem  nfopab1 4628 
The first abstraction variable in an orderedpair class abstraction
(class builder) is effectively not free. (Contributed by NM,
16May1995.) (Revised by Mario Carneiro, 14Oct2016.)

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

Theorem  nfopab2 4629 
The second abstraction variable in an orderedpair class abstraction
(class builder) is effectively not free. (Contributed by NM,
16May1995.) (Revised by Mario Carneiro, 14Oct2016.)

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

Theorem  cbvopab 4630* 
Rule used to change bound variables in an orderedpair class
abstraction, using implicit substitution. (Contributed by NM,
14Sep2003.)

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

Theorem  cbvopabv 4631* 
Rule used to change bound variables in an orderedpair class
abstraction, using implicit substitution. (Contributed by NM,
15Oct1996.)

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

Theorem  cbvopab1 4632* 
Change first bound variable in an orderedpair class abstraction, using
explicit substitution. (Contributed by NM, 6Oct2004.) (Revised by
Mario Carneiro, 14Oct2016.)

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

Theorem  cbvopab2 4633* 
Change second bound variable in an orderedpair class abstraction, using
explicit substitution. (Contributed by NM, 22Aug2013.)

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

Theorem  cbvopab1s 4634* 
Change first bound variable in an orderedpair class abstraction, using
explicit substitution. (Contributed by NM, 31Jul2003.)

⊢ {⟨x, y⟩ ∣ φ} = {⟨z, y⟩ ∣ [z /
x]φ} 

Theorem  cbvopab1v 4635* 
Rule used to change the first bound variable in an ordered pair
abstraction, using implicit substitution. (Contributed by NM,
31Jul2003.) (Proof shortened by Eric Schmidt, 4Apr2007.)

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

Theorem  cbvopab2v 4636* 
Rule used to change the second bound variable in an ordered pair
abstraction, using implicit substitution. (Contributed by NM,
2Sep1999.)

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

Theorem  csbopabg 4637* 
Move substitution into a class abstraction. (Contributed by NM,
6Aug2007.) (Proof shortened by Mario Carneiro, 17Nov2016.)

⊢ (A ∈ V →
[A / x]{⟨y, z⟩ ∣ φ} =
{⟨y,
z⟩ ∣ [̣A /
x]̣φ}) 

Theorem  unopab 4638 
Union of two ordered pair class abstractions. (Contributed by NM,
30Sep2002.)

⊢ ({⟨x, y⟩ ∣ φ} ∪ {⟨x, y⟩ ∣ ψ}) =
{⟨x,
y⟩ ∣ (φ
∨ ψ)} 

2.3.3 Binary relations


Syntax  wbr 4639 
Extend wff notation to include the general binary relation predicate.
Note that the syntax is simply three class symbols in a row. Since binary
relations are the only possible wff expressions consisting of three class
expressions in a row, the syntax is unambiguous.

wff
ARB 

Definition  dfbr 4640 
Define a general binary relation. Note that the syntax is simply three
class symbols in a row. Definition 6.18 of [TakeutiZaring] p. 29
generalized to arbitrary classes. Class R normally denotes a relation
that compares two classes A and B. 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 R is a proper class. (Contributed
by NM, 4Jun1995.)

⊢ (ARB ↔ ⟨A, B⟩ ∈ R) 

Theorem  breq 4641 
Equality theorem for binary relations. (Contributed by NM,
4Jun1995.)

⊢ (R =
S → (ARB ↔ ASB)) 

Theorem  breq1 4642 
Equality theorem for a binary relation. (Contributed by NM,
31Dec1993.)

⊢ (A =
B → (ARC ↔ BRC)) 

Theorem  breq2 4643 
Equality theorem for a binary relation. (Contributed by NM,
31Dec1993.)

⊢ (A =
B → (CRA ↔ CRB)) 

Theorem  breq12 4644 
Equality theorem for a binary relation. (Contributed by NM,
8Feb1996.)

⊢ ((A =
B ∧
C = D)
→ (ARC ↔
BRD)) 

Theorem  breqi 4645 
Equality inference for binary relations. (Contributed by NM,
19Feb2005.)

⊢ R =
S ⇒ ⊢ (ARB ↔
ASB) 

Theorem  breq1i 4646 
Equality inference for a binary relation. (Contributed by NM,
8Feb1996.)

⊢ A =
B ⇒ ⊢ (ARC ↔
BRC) 

Theorem  breq2i 4647 
Equality inference for a binary relation. (Contributed by NM,
8Feb1996.)

⊢ A =
B ⇒ ⊢ (CRA ↔
CRB) 

Theorem  breq12i 4648 
Equality inference for a binary relation. (Contributed by NM,
8Feb1996.) (Revised by Eric Schmidt, 4Apr2007.)

⊢ A =
B
& ⊢ C =
D ⇒ ⊢ (ARC ↔
BRD) 

Theorem  breq1d 4649 
Equality deduction for a binary relation. (Contributed by NM,
8Feb1996.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (ARC ↔
BRC)) 

Theorem  breqd 4650 
Equality deduction for a binary relation. (Contributed by NM,
29Oct2011.)

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

Theorem  breq2d 4651 
Equality deduction for a binary relation. (Contributed by NM,
8Feb1996.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (CRA ↔
CRB)) 

Theorem  breq12d 4652 
Equality deduction for a binary relation. (The proof was shortened by
Andrew Salmon, 9Jul2011.) (Contributed by NM, 8Feb1996.)
(Revised by set.mm contributors, 9Jul2011.)

⊢ (φ
→ A = B)
& ⊢ (φ
→ C = D) ⇒ ⊢ (φ
→ (ARC ↔
BRD)) 

Theorem  breq123d 4653 
Equality deduction for a binary relation. (Contributed by NM,
29Oct2011.)

⊢ (φ
→ A = B)
& ⊢ (φ
→ R = S)
& ⊢ (φ
→ C = D) ⇒ ⊢ (φ
→ (ARC ↔
BSD)) 

Theorem  breqan12d 4654 
Equality deduction for a binary relation. (Contributed by NM,
8Feb1996.)

⊢ (φ
→ A = B)
& ⊢ (ψ
→ C = D) ⇒ ⊢ ((φ
∧ ψ)
→ (ARC ↔
BRD)) 

Theorem  breqan12rd 4655 
Equality deduction for a binary relation. (Contributed by NM,
8Feb1996.)

⊢ (φ
→ A = B)
& ⊢ (ψ
→ C = D) ⇒ ⊢ ((ψ
∧ φ)
→ (ARC ↔
BRD)) 

Theorem  nbrne1 4656 
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3Jun2012.)

⊢ ((ARB ∧ ¬ ARC) → B
≠ C) 

Theorem  nbrne2 4657 
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3Jun2012.)

⊢ ((ARC ∧ ¬ BRC) → A
≠ B) 

Theorem  eqbrtri 4658 
Substitution of equal classes into a binary relation. (Contributed by
NM, 5Aug1993.)

⊢ A =
B
& ⊢ BRC ⇒ ⊢ ARC 

Theorem  eqbrtrd 4659 
Substitution of equal classes into a binary relation. (Contributed by
NM, 8Oct1999.)

⊢ (φ
→ A = B)
& ⊢ (φ
→ BRC) ⇒ ⊢ (φ
→ ARC) 

Theorem  eqbrtrri 4660 
Substitution of equal classes into a binary relation. (Contributed by
NM, 5Aug1993.)

⊢ A =
B
& ⊢ ARC ⇒ ⊢ BRC 

Theorem  eqbrtrrd 4661 
Substitution of equal classes into a binary relation. (Contributed by
NM, 24Oct1999.)

⊢ (φ
→ A = B)
& ⊢ (φ
→ ARC) ⇒ ⊢ (φ
→ BRC) 

Theorem  breqtri 4662 
Substitution of equal classes into a binary relation. (Contributed by
NM, 5Aug1993.)

⊢ ARB & ⊢ B =
C ⇒ ⊢ ARC 

Theorem  breqtrd 4663 
Substitution of equal classes into a binary relation. (Contributed by
NM, 24Oct1999.)

⊢ (φ
→ ARB) & ⊢ (φ
→ B = C) ⇒ ⊢ (φ
→ ARC) 

Theorem  breqtrri 4664 
Substitution of equal classes into a binary relation. (Contributed by
NM, 5Aug1993.)

⊢ ARB & ⊢ C =
B ⇒ ⊢ ARC 

Theorem  breqtrrd 4665 
Substitution of equal classes into a binary relation. (Contributed by
NM, 24Oct1999.)

⊢ (φ
→ ARB) & ⊢ (φ
→ C = B) ⇒ ⊢ (φ
→ ARC) 

Theorem  3brtr3i 4666 
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11Aug1999.)

⊢ ARB & ⊢ A =
C
& ⊢ B =
D ⇒ ⊢ CRD 

Theorem  3brtr4i 4667 
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11Aug1999.)

⊢ ARB & ⊢ C =
A
& ⊢ D =
B ⇒ ⊢ CRD 

Theorem  3brtr3d 4668 
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 18Oct1999.)

⊢ (φ
→ ARB) & ⊢ (φ
→ A = C)
& ⊢ (φ
→ B = D) ⇒ ⊢ (φ
→ CRD) 

Theorem  3brtr4d 4669 
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 21Feb2005.)

⊢ (φ
→ ARB) & ⊢ (φ
→ C = A)
& ⊢ (φ
→ D = B) ⇒ ⊢ (φ
→ CRD) 

Theorem  3brtr3g 4670 
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16Jan1997.)

⊢ (φ
→ ARB) & ⊢ A =
C
& ⊢ B =
D ⇒ ⊢ (φ
→ CRD) 

Theorem  3brtr4g 4671 
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16Jan1997.)

⊢ (φ
→ ARB) & ⊢ C =
A
& ⊢ D =
B ⇒ ⊢ (φ
→ CRD) 

Theorem  syl5eqbr 4672 
B chained equality inference for a binary relation. (Contributed by NM,
11Oct1999.)

⊢ A =
B
& ⊢ (φ
→ BRC) ⇒ ⊢ (φ
→ ARC) 

Theorem  syl5eqbrr 4673 
B chained equality inference for a binary relation. (Contributed by NM,
17Sep2004.)

⊢ B =
A
& ⊢ (φ
→ BRC) ⇒ ⊢ (φ
→ ARC) 

Theorem  syl5breq 4674 
B chained equality inference for a binary relation. (Contributed by NM,
11Oct1999.)

⊢ ARB & ⊢ (φ
→ B = C) ⇒ ⊢ (φ
→ ARC) 

Theorem  syl5breqr 4675 
B chained equality inference for a binary relation. (Contributed by NM,
24Apr2005.)

⊢ ARB & ⊢ (φ
→ C = B) ⇒ ⊢ (φ
→ ARC) 

Theorem  syl6eqbr 4676 
A chained equality inference for a binary relation. (Contributed by NM,
12Oct1999.)

⊢ (φ
→ A = B)
& ⊢ BRC ⇒ ⊢ (φ
→ ARC) 

Theorem  syl6eqbrr 4677 
A chained equality inference for a binary relation. (Contributed by NM,
4Jan2006.)

⊢ (φ
→ B = A)
& ⊢ BRC ⇒ ⊢ (φ
→ ARC) 

Theorem  syl6breq 4678 
A chained equality inference for a binary relation. (Contributed by NM,
11Oct1999.)

⊢ (φ
→ ARB) & ⊢ B =
C ⇒ ⊢ (φ
→ ARC) 

Theorem  syl6breqr 4679 
A chained equality inference for a binary relation. (Contributed by NM,
24Apr2005.)

⊢ (φ
→ ARB) & ⊢ C =
B ⇒ ⊢ (φ
→ ARC) 

Theorem  ssbrd 4680 
Deduction from a subclass relationship of binary relations.
(Contributed by NM, 30Apr2004.)

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

Theorem  ssbri 4681 
Inference from a subclass relationship of binary relations. (The proof
was shortened by Andrew Salmon, 9Jul2011.) (Contributed by NM,
28Mar2007.) (Revised by set.mm contributors, 9Jul2011.)

⊢ A ⊆ B ⇒ ⊢ (CAD →
CBD) 

Theorem  nfbrd 4682 
Deduction version of boundvariable hypothesis builder nfbr 4683.
(Contributed by NM, 13Dec2005.) (Revised by Mario Carneiro,
14Oct2016.)

⊢ (φ
→ ℲxA)
& ⊢ (φ
→ ℲxR)
& ⊢ (φ
→ ℲxB) ⇒ ⊢ (φ
→ Ⅎx ARB) 

Theorem  nfbr 4683 
Boundvariable hypothesis builder for binary relation. (Contributed by
NM, 1Sep1999.) (Revised by Mario Carneiro, 14Oct2016.)

⊢ ℲxA & ⊢ ℲxR & ⊢ ℲxB ⇒ ⊢ Ⅎx
ARB 

Theorem  brab1 4684* 
Relationship between a binary relation and a class abstraction.
(Contributed by Andrew Salmon, 8Jul2011.)

⊢ (xRA ↔
x ∈
{z ∣
zRA}) 

Theorem  sbcbrg 4685 
Move substitution in and out of a binary relation. (Contributed by NM,
13Dec2005.) (Proof shortened by Andrew Salmon, 9Jul2011.)

⊢ (A ∈ D →
([̣A / x]̣BRC ↔ [A / x]B[A /
x]R[A /
x]C)) 

Theorem  sbcbr12g 4686* 
Move substitution in and out of a binary relation. (Contributed by NM,
13Dec2005.)

⊢ (A ∈ D →
([̣A / x]̣BRC ↔ [A / x]BR[A /
x]C)) 

Theorem  sbcbr1g 4687* 
Move substitution in and out of a binary relation. (Contributed by NM,
13Dec2005.)

⊢ (A ∈ D →
([̣A / x]̣BRC ↔ [A / x]BRC)) 

Theorem  sbcbr2g 4688* 
Move substitution in and out of a binary relation. (Contributed by NM,
13Dec2005.)

⊢ (A ∈ D →
([̣A / x]̣BRC ↔ BR[A /
x]C)) 

Theorem  brex 4689 
Binary relationship implies sethood of both parts. (Contributed by SF,
7Jan2015.)

⊢ (ARB →
(A ∈ V
∧ B ∈ V)) 

Theorem  brreldmex 4690 
Binary relationship implies sethood of domain. (Contributed by SF,
7Jan2018.)

⊢ (ARB →
A ∈
V) 

Theorem  brrelrnex 4691 
Binary relationship implies sethood of range. (Contributed by SF,
7Jan2018.)

⊢ (ARB →
B ∈
V) 

Theorem  brun 4692 
The union of two binary relations. (Contributed by NM, 21Dec2008.)

⊢ (A(R ∪ S)B ↔
(ARB ∨ ASB)) 

Theorem  brin 4693 
The intersection of two relations. (Contributed by FL, 7Oct2008.)

⊢ (A(R ∩ S)B ↔
(ARB ∧ ASB)) 

Theorem  brdif 4694 
The difference of two binary relations. (Contributed by Scott Fenton,
11Apr2011.)

⊢ (A(R ∖ S)B ↔
(ARB ∧ ¬ ASB)) 

2.3.4 Orderedpair class abstractions
(cont.)


Theorem  opabid 4695 
The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
(The proof was shortened by Andrew Salmon, 25Jul2011.) (Contributed
by NM, 14Apr1995.) (Revised by set.mm contributors, 25Jul2011.)

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

Theorem  elopab 4696* 
Membership in a class abstraction of pairs. (Contributed by NM,
24Mar1998.)

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

Theorem  opelopabsb 4697* 
The law of concretion in terms of substitutions. (Contributed by NM,
30Sep2002.) (Revised by Mario Carneiro, 18Nov2016.)

⊢ (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ}
↔ [̣A / x]̣[̣B / y]̣φ) 

Theorem  brabsb 4698* 
The law of concretion in terms of substitutions. (Contributed by NM,
17Mar2008.)

⊢ R = {⟨x, y⟩ ∣ φ} ⇒ ⊢ (ARB ↔
[̣A / x]̣[̣B / y]̣φ) 

Theorem  opelopabt 4699* 
Closed theorem form of opelopab 4708. (Contributed by NM,
19Feb2013.)

⊢ ((∀x∀y(x = A → (φ
↔ ψ)) ∧ ∀x∀y(y = B → (ψ
↔ χ)) ∧ (A ∈ V ∧ B ∈ W)) →
(⟨A,
B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ χ)) 

Theorem  opelopabga 4700* 
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
Mario Carneiro, 19Dec2013.)

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