Type  Label  Description 
Statement 

Theorem  nnsuc 4401* 
A nonzero natural number is a successor. (Contributed by NM,
18Feb2004.)

⊢ ((𝐴 ∈ ω ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥) 

Theorem  nndceq0 4402 
A natural number is either zero or nonzero. Decidable equality for
natural numbers is a special case of the law of the excluded middle
which holds in most constructive set theories including ours.
(Contributed by Jim Kingdon, 5Jan2019.)

⊢ (𝐴 ∈ ω → DECID
𝐴 =
∅) 

Theorem  0elnn 4403 
A natural number is either the empty set or has the empty set as an
element. (Contributed by Jim Kingdon, 23Aug2019.)

⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∅ ∈ 𝐴)) 

Theorem  nn0eln0 4404 
A natural number is nonempty iff it contains the empty set. Although in
constructive mathematics it is generally more natural to work with
inhabited sets and ignore the whole concept of nonempty sets, in the
specific case of natural numbers this theorem may be helpful in converting
proofs which were written assuming excluded middle. (Contributed by Jim
Kingdon, 28Aug2019.)

⊢ (𝐴 ∈ ω → (∅ ∈
𝐴 ↔ 𝐴 ≠ ∅)) 

Theorem  nnregexmid 4405* 
If inhabited sets of natural numbers always have minimal elements,
excluded middle follows. The argument is essentially the same as
regexmid 4322 and the larger lesson is that although
natural numbers may
behave "nonconstructively" even in a constructive set theory
(for
example see nndceq 6207 or nntri3or 6201), sets of natural numbers are a
different animal. (Contributed by Jim Kingdon, 6Sep2019.)

⊢ ((𝑥 ⊆ ω ∧ ∃𝑦 𝑦 ∈ 𝑥) → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) 

Theorem  omsinds 4406* 
Strong (or "total") induction principle over ω. (Contributed by
Scott Fenton, 17Jul2015.)

⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 ∈ ω →
(∀𝑦 ∈ 𝑥 𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ ω → 𝜒) 

2.6.6 Relations


Syntax  cxp 4407 
Extend the definition of a class to include the cross product.

class (𝐴 × 𝐵) 

Syntax  ccnv 4408 
Extend the definition of a class to include the converse of a class.

class ^{◡}𝐴 

Syntax  cdm 4409 
Extend the definition of a class to include the domain of a class.

class dom 𝐴 

Syntax  crn 4410 
Extend the definition of a class to include the range of a class.

class ran 𝐴 

Syntax  cres 4411 
Extend the definition of a class to include the restriction of a class.
(Read: The restriction of 𝐴 to 𝐵.)

class (𝐴 ↾ 𝐵) 

Syntax  cima 4412 
Extend the definition of a class to include the image of a class. (Read:
The image of 𝐵 under 𝐴.)

class (𝐴 “ 𝐵) 

Syntax  ccom 4413 
Extend the definition of a class to include the composition of two
classes. (Read: The composition of 𝐴 and 𝐵.)

class (𝐴 ∘ 𝐵) 

Syntax  wrel 4414 
Extend the definition of a wff to include the relation predicate. (Read:
𝐴 is a relation.)

wff Rel 𝐴 

Definition  dfxp 4415* 
Define the cross product of two classes. Definition 9.11 of [Quine]
p. 64. For example, ( { 1 , 5 } × { 2 , 7
} ) = ( { ⟨ 1 , 2
⟩, ⟨ 1 , 7
⟩ } ∪ { ⟨ 5 , 2 ⟩, ⟨ 5 ,
7 ⟩ } ) . Another example is that the set
of rational numbers are
defined in using the crossproduct ( Z × N
) ; the left and
righthand sides of the crossproduct represent the top (integer) and
bottom (natural) numbers of a fraction. (Contributed by NM,
4Jul1994.)

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

Definition  dfrel 4416 
Define the relation predicate. Definition 6.4(1) of [TakeutiZaring]
p. 23. For alternate definitions, see dfrel2 4843 and dfrel3 4850.
(Contributed by NM, 1Aug1994.)

⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) 

Definition  dfcnv 4417* 
Define the converse of a class. Definition 9.12 of [Quine] p. 64. The
converse of a binary relation swaps its arguments, i.e., if 𝐴 ∈
V
and 𝐵 ∈ V then (𝐴^{◡}𝑅𝐵 ↔ 𝐵𝑅𝐴), as proven in brcnv 4585
(see dfbr 3820 and dfrel 4416 for more on relations). For example, ^{◡}
{ ⟨ 2 , 6 ⟩,
⟨ 3 , 9 ⟩ } = { ⟨ 6 , 2 ⟩,
⟨ 9 , 3 ⟩ } .
We use Quine's breve accent (smile) notation.
Like Quine, we use it as a prefix, which eliminates the need for
parentheses. Many authors use the postfix superscript "to the
minus
one." "Converse" is Quine's terminology; some authors
call it
"inverse," especially when the argument is a function.
(Contributed by
NM, 4Jul1994.)

⊢ ^{◡}𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} 

Definition  dfco 4418* 
Define the composition of two classes. Definition 6.6(3) of
[TakeutiZaring] p. 24. Note that
Definition 7 of [Suppes] p. 63
reverses 𝐴 and 𝐵, uses a slash instead of
∘, and calls
the operation "relative product." (Contributed by NM,
4Jul1994.)

⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} 

Definition  dfdm 4419* 
Define the domain of a class. Definition 3 of [Suppes] p. 59. For
example, F = { ⟨ 2 , 6 ⟩, ⟨ 3 , 9 ⟩ } → dom F
= { 2 , 3 } . Contrast with range (defined in dfrn 4420). For alternate
definitions see dfdm2 4927, dfdm3 4589, and dfdm4 4594. The
notation "dom " is used by Enderton;
other authors sometimes use
script D. (Contributed by NM, 1Aug1994.)

⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} 

Definition  dfrn 4420 
Define the range of a class. For example, F = { ⟨
2 , 6 ⟩,
⟨ 3 , 9 ⟩ }
> ran F = { 6 , 9 } . Contrast with domain
(defined in dfdm 4419). For alternate definitions, see dfrn2 4590,
dfrn3 4591, and dfrn4 4853. The notation "ran " is used by Enderton;
other authors sometimes use script R or script W. (Contributed by NM,
1Aug1994.)

⊢ ran 𝐴 = dom ^{◡}𝐴 

Definition  dfres 4421 
Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring]
p. 24. For example ( F = { ⟨ 2 , 6 ⟩, ⟨ 3 , 9 ⟩ }
∧ B = { 1 , 2 } ) > ( F ↾ B ) = { ⟨ 2 , 6 ⟩ } .
(Contributed by NM, 2Aug1994.)

⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) 

Definition  dfima 4422 
Define the image of a class (as restricted by another class).
Definition 6.6(2) of [TakeutiZaring] p. 24. For example, ( F = {
⟨
2 , 6 ⟩, ⟨ 3 ,
9 ⟩ } /\ B = { 1 , 2 } ) > ( F “ B )
= { 6 } . Contrast with restriction (dfres 4421) and range (dfrn 4420).
For an alternate definition, see dfima2 4739. (Contributed by NM,
2Aug1994.)

⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) 

Theorem  xpeq1 4423 
Equality theorem for cross product. (Contributed by NM, 4Jul1994.)

⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) 

Theorem  xpeq2 4424 
Equality theorem for cross product. (Contributed by NM, 5Jul1994.)

⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) 

Theorem  elxpi 4425* 
Membership in a cross product. Uses fewer axioms than elxp 4426.
(Contributed by NM, 4Jul1994.)

⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) 

Theorem  elxp 4426* 
Membership in a cross product. (Contributed by NM, 4Jul1994.)

⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) 

Theorem  elxp2 4427* 
Membership in a cross product. (Contributed by NM, 23Feb2004.)

⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐴 = ⟨𝑥, 𝑦⟩) 

Theorem  xpeq12 4428 
Equality theorem for cross product. (Contributed by FL, 31Aug2009.)

⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷)) 

Theorem  xpeq1i 4429 
Equality inference for cross product. (Contributed by NM,
21Dec2008.)

⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 × 𝐶) = (𝐵 × 𝐶) 

Theorem  xpeq2i 4430 
Equality inference for cross product. (Contributed by NM,
21Dec2008.)

⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 × 𝐴) = (𝐶 × 𝐵) 

Theorem  xpeq12i 4431 
Equality inference for cross product. (Contributed by FL,
31Aug2009.)

⊢ 𝐴 = 𝐵
& ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 × 𝐶) = (𝐵 × 𝐷) 

Theorem  xpeq1d 4432 
Equality deduction for cross product. (Contributed by Jeff Madsen,
17Jun2010.)

⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) 

Theorem  xpeq2d 4433 
Equality deduction for cross product. (Contributed by Jeff Madsen,
17Jun2010.)

⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵)) 

Theorem  xpeq12d 4434 
Equality deduction for cross product. (Contributed by NM,
8Dec2013.)

⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷)) 

Theorem  nfxp 4435 
Boundvariable hypothesis builder for cross product. (Contributed by
NM, 15Sep2003.) (Revised by Mario Carneiro, 15Oct2016.)

⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 × 𝐵) 

Theorem  0nelxp 4436 
The empty set is not a member of a cross product. (Contributed by NM,
2May1996.) (Revised by Mario Carneiro, 26Apr2015.)

⊢ ¬ ∅ ∈ (𝐴 × 𝐵) 

Theorem  0nelelxp 4437 
A member of a cross product (ordered pair) doesn't contain the empty
set. (Contributed by NM, 15Dec2008.)

⊢ (𝐶 ∈ (𝐴 × 𝐵) → ¬ ∅ ∈ 𝐶) 

Theorem  opelxp 4438 
Ordered pair membership in a cross product. (Contributed by NM,
15Nov1994.) (Proof shortened by Andrew Salmon, 12Aug2011.)
(Revised by Mario Carneiro, 26Apr2015.)

⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) 

Theorem  brxp 4439 
Binary relation on a cross product. (Contributed by NM,
22Apr2004.)

⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) 

Theorem  opelxpi 4440 
Ordered pair membership in a cross product (implication). (Contributed by
NM, 28May1995.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷)) 

Theorem  opelxp1 4441 
The first member of an ordered pair of classes in a cross product belongs
to first cross product argument. (Contributed by NM, 28May2008.)
(Revised by Mario Carneiro, 26Apr2015.)

⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) → 𝐴 ∈ 𝐶) 

Theorem  opelxp2 4442 
The second member of an ordered pair of classes in a cross product belongs
to second cross product argument. (Contributed by Mario Carneiro,
26Apr2015.)

⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) → 𝐵 ∈ 𝐷) 

Theorem  otelxp1 4443 
The first member of an ordered triple of classes in a cross product
belongs to first cross product argument. (Contributed by NM,
28May2008.)

⊢ (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ ((𝑅 × 𝑆) × 𝑇) → 𝐴 ∈ 𝑅) 

Theorem  rabxp 4444* 
Membership in a class builder restricted to a cross product.
(Contributed by NM, 20Feb2014.)

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

Theorem  brrelex12 4445 
A true binary relation on a relation implies the arguments are sets.
(This is a property of our ordered pair definition.) (Contributed by
Mario Carneiro, 26Apr2015.)

⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) 

Theorem  brrelex 4446 
A true binary relation on a relation implies the first argument is a set.
(This is a property of our ordered pair definition.) (Contributed by NM,
18May2004.) (Revised by Mario Carneiro, 26Apr2015.)

⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V) 

Theorem  brrelex2 4447 
A true binary relation on a relation implies the second argument is a set.
(This is a property of our ordered pair definition.) (Contributed by
Mario Carneiro, 26Apr2015.)

⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V) 

Theorem  brrelexi 4448 
The first argument of a binary relation exists. (An artifact of our
ordered pair definition.) (Contributed by NM, 4Jun1998.)

⊢ Rel 𝑅 ⇒ ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V) 

Theorem  brrelex2i 4449 
The second argument of a binary relation exists. (An artifact of our
ordered pair definition.) (Contributed by Mario Carneiro,
26Apr2015.)

⊢ Rel 𝑅 ⇒ ⊢ (𝐴𝑅𝐵 → 𝐵 ∈ V) 

Theorem  nprrel 4450 
No proper class is related to anything via any relation. (Contributed
by Roy F. Longton, 30Jul2005.)

⊢ Rel 𝑅
& ⊢ ¬ 𝐴 ∈ V ⇒ ⊢ ¬ 𝐴𝑅𝐵 

Theorem  fconstmpt 4451* 
Representation of a constant function using the mapping operation.
(Note that 𝑥 cannot appear free in 𝐵.)
(Contributed by NM,
12Oct1999.) (Revised by Mario Carneiro, 16Nov2013.)

⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵) 

Theorem  vtoclr 4452* 
Variable to class conversion of transitive relation. (Contributed by
NM, 9Jun1998.) (Revised by Mario Carneiro, 26Apr2015.)

⊢ Rel 𝑅
& ⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ⇒ ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) 

Theorem  opelvvg 4453 
Ordered pair membership in the universal class of ordered pairs.
(Contributed by Mario Carneiro, 3May2015.)

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

Theorem  opelvv 4454 
Ordered pair membership in the universal class of ordered pairs.
(Contributed by NM, 22Aug2013.) (Revised by Mario Carneiro,
26Apr2015.)

⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ⟨𝐴, 𝐵⟩ ∈ (V ×
V) 

Theorem  opthprc 4455 
Justification theorem for an ordered pair definition that works for any
classes, including proper classes. This is a possible definition
implied by the footnote in [Jech] p. 78,
which says, "The sophisticated
reader will not object to our use of a pair of classes."
(Contributed
by NM, 28Sep2003.)

⊢ (((𝐴 × {∅}) ∪ (𝐵 × {{∅}})) =
((𝐶 × {∅})
∪ (𝐷 ×
{{∅}})) ↔ (𝐴 =
𝐶 ∧ 𝐵 = 𝐷)) 

Theorem  brel 4456 
Two things in a binary relation belong to the relation's domain.
(Contributed by NM, 17May1996.) (Revised by Mario Carneiro,
26Apr2015.)

⊢ 𝑅 ⊆ (𝐶 × 𝐷) ⇒ ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) 

Theorem  brab2a 4457* 
Ordered pair membership in an ordered pair class abstraction.
(Contributed by Mario Carneiro, 9Nov2015.)

⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ⇒ ⊢ (𝐴𝑅𝐵 ↔ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ 𝜓)) 

Theorem  elxp3 4458* 
Membership in a cross product. (Contributed by NM, 5Mar1995.)

⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(⟨𝑥, 𝑦⟩ = 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐵 × 𝐶))) 

Theorem  opeliunxp 4459 
Membership in a union of cross products. (Contributed by Mario
Carneiro, 29Dec2014.) (Revised by Mario Carneiro, 1Jan2017.)

⊢ (⟨𝑥, 𝐶⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵)) 

Theorem  xpundi 4460 
Distributive law for cross product over union. Theorem 103 of [Suppes]
p. 52. (Contributed by NM, 12Aug2004.)

⊢ (𝐴 × (𝐵 ∪ 𝐶)) = ((𝐴 × 𝐵) ∪ (𝐴 × 𝐶)) 

Theorem  xpundir 4461 
Distributive law for cross product over union. Similar to Theorem 103
of [Suppes] p. 52. (Contributed by NM,
30Sep2002.)

⊢ ((𝐴 ∪ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) 

Theorem  xpiundi 4462* 
Distributive law for cross product over indexed union. (Contributed by
Mario Carneiro, 27Apr2014.)

⊢ (𝐶 × ∪ 𝑥 ∈ 𝐴 𝐵) = ∪
𝑥 ∈ 𝐴 (𝐶 × 𝐵) 

Theorem  xpiundir 4463* 
Distributive law for cross product over indexed union. (Contributed by
Mario Carneiro, 27Apr2014.)

⊢ (∪ 𝑥 ∈ 𝐴 𝐵 × 𝐶) = ∪
𝑥 ∈ 𝐴 (𝐵 × 𝐶) 

Theorem  iunxpconst 4464* 
Membership in a union of cross products when the second factor is
constant. (Contributed by Mario Carneiro, 29Dec2014.)

⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵) 

Theorem  xpun 4465 
The cross product of two unions. (Contributed by NM, 12Aug2004.)

⊢ ((𝐴 ∪ 𝐵) × (𝐶 ∪ 𝐷)) = (((𝐴 × 𝐶) ∪ (𝐴 × 𝐷)) ∪ ((𝐵 × 𝐶) ∪ (𝐵 × 𝐷))) 

Theorem  elvv 4466* 
Membership in universal class of ordered pairs. (Contributed by NM,
4Jul1994.)

⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩) 

Theorem  elvvv 4467* 
Membership in universal class of ordered triples. (Contributed by NM,
17Dec2008.)

⊢ (𝐴 ∈ ((V × V) × V) ↔
∃𝑥∃𝑦∃𝑧 𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) 

Theorem  elvvuni 4468 
An ordered pair contains its union. (Contributed by NM,
16Sep2006.)

⊢ (𝐴 ∈ (V × V) → ∪ 𝐴
∈ 𝐴) 

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

⊢ (∀𝑦∀𝑧∃*𝑥𝜑 → ∃*𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)) 

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

⊢ ∃*𝑥𝜑 ⇒ ⊢ ∃*𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑) 

Theorem  brinxp2 4471 
Intersection of binary relation with cross product. (Contributed by NM,
3Mar2007.) (Revised by Mario Carneiro, 26Apr2015.)

⊢ (𝐴(𝑅 ∩ (𝐶 × 𝐷))𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵)) 

Theorem  brinxp 4472 
Intersection of binary relation with cross product. (Contributed by NM,
9Mar1997.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝑅𝐵 ↔ 𝐴(𝑅 ∩ (𝐶 × 𝐷))𝐵)) 

Theorem  poinxp 4473 
Intersection of partial order with cross product of its field.
(Contributed by Mario Carneiro, 10Jul2014.)

⊢ (𝑅 Po 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) Po 𝐴) 

Theorem  soinxp 4474 
Intersection of linear order with cross product of its field.
(Contributed by Mario Carneiro, 10Jul2014.)

⊢ (𝑅 Or 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) Or 𝐴) 

Theorem  seinxp 4475 
Intersection of setlike relation with cross product of its field.
(Contributed by Mario Carneiro, 22Jun2015.)

⊢ (𝑅 Se 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) Se 𝐴) 

Theorem  posng 4476 
Partial ordering of a singleton. (Contributed by Jim Kingdon,
5Dec2018.)

⊢ ((Rel 𝑅 ∧ 𝐴 ∈ V) → (𝑅 Po {𝐴} ↔ ¬ 𝐴𝑅𝐴)) 

Theorem  sosng 4477 
Strict linear ordering on a singleton. (Contributed by Jim Kingdon,
5Dec2018.)

⊢ ((Rel 𝑅 ∧ 𝐴 ∈ V) → (𝑅 Or {𝐴} ↔ ¬ 𝐴𝑅𝐴)) 

Theorem  opabssxp 4478* 
An abstraction relation is a subset of a related cross product.
(Contributed by NM, 16Jul1995.)

⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) 

Theorem  brab2ga 4479* 
The law of concretion for a binary relation. See brab2a 4457 for alternate
proof. TODO: should one of them be deleted? (Contributed by Mario
Carneiro, 28Apr2015.) (Proof modification is discouraged.)

⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ⇒ ⊢ (𝐴𝑅𝐵 ↔ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ 𝜓)) 

Theorem  optocl 4480* 
Implicit substitution of class for ordered pair. (Contributed by NM,
5Mar1995.)

⊢ 𝐷 = (𝐵 × 𝐶)
& ⊢ (⟨𝑥, 𝑦⟩ = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝐷 → 𝜓) 

Theorem  2optocl 4481* 
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12Mar1995.)

⊢ 𝑅 = (𝐶 × 𝐷)
& ⊢ (⟨𝑥, 𝑦⟩ = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (⟨𝑧, 𝑤⟩ = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅) → 𝜒) 

Theorem  3optocl 4482* 
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12Mar1995.)

⊢ 𝑅 = (𝐷 × 𝐹)
& ⊢ (⟨𝑥, 𝑦⟩ = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (⟨𝑧, 𝑤⟩ = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (⟨𝑣, 𝑢⟩ = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐹) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑅) → 𝜃) 

Theorem  opbrop 4483* 
Ordered pair membership in a relation. Special case. (Contributed by
NM, 5Aug1995.)

⊢ (((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ (𝑣 = 𝐶 ∧ 𝑢 = 𝐷)) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ 𝜑))} ⇒ ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ 𝜓)) 

Theorem  0xp 4484 
The cross product with the empty set is empty. Part of Theorem 3.13(ii)
of [Monk1] p. 37. (Contributed by NM,
4Jul1994.)

⊢ (∅ × 𝐴) = ∅ 

Theorem  csbxpg 4485 
Distribute proper substitution through the cross product of two classes.
(Contributed by Alan Sare, 10Nov2012.)

⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶)) 

Theorem  releq 4486 
Equality theorem for the relation predicate. (Contributed by NM,
1Aug1994.)

⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵)) 

Theorem  releqi 4487 
Equality inference for the relation predicate. (Contributed by NM,
8Dec2006.)

⊢ 𝐴 = 𝐵 ⇒ ⊢ (Rel 𝐴 ↔ Rel 𝐵) 

Theorem  releqd 4488 
Equality deduction for the relation predicate. (Contributed by NM,
8Mar2014.)

⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Rel 𝐴 ↔ Rel 𝐵)) 

Theorem  nfrel 4489 
Boundvariable hypothesis builder for a relation. (Contributed by NM,
31Jan2004.) (Revised by Mario Carneiro, 15Oct2016.)

⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥Rel 𝐴 

Theorem  sbcrel 4490 
Distribute proper substitution through a relation predicate. (Contributed
by Alexander van der Vekens, 23Jul2017.)

⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Rel 𝑅 ↔ Rel ⦋𝐴 / 𝑥⦌𝑅)) 

Theorem  relss 4491 
Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58.
(Contributed by NM, 15Aug1994.)

⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴)) 

Theorem  ssrel 4492* 
A subclass relationship depends only on a relation's ordered pairs.
Theorem 3.2(i) of [Monk1] p. 33.
(Contributed by NM, 2Aug1994.)
(Proof shortened by Andrew Salmon, 27Aug2011.)

⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))) 

Theorem  eqrel 4493* 
Extensionality principle for relations. Theorem 3.2(ii) of [Monk1]
p. 33. (Contributed by NM, 2Aug1994.)

⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))) 

Theorem  ssrel2 4494* 
A subclass relationship depends only on a relation's ordered pairs.
This version of ssrel 4492 is restricted to the relation's domain.
(Contributed by Thierry Arnoux, 25Jan2018.)

⊢ (𝑅 ⊆ (𝐴 × 𝐵) → (𝑅 ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (⟨𝑥, 𝑦⟩ ∈ 𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))) 

Theorem  relssi 4495* 
Inference from subclass principle for relations. (Contributed by NM,
31Mar1998.)

⊢ Rel 𝐴
& ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) ⇒ ⊢ 𝐴 ⊆ 𝐵 

Theorem  relssdv 4496* 
Deduction from subclass principle for relations. (Contributed by NM,
11Sep2004.)

⊢ (𝜑 → Rel 𝐴)
& ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) 

Theorem  eqrelriv 4497* 
Inference from extensionality principle for relations. (Contributed by
FL, 15Oct2012.)

⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵) ⇒ ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵) 

Theorem  eqrelriiv 4498* 
Inference from extensionality principle for relations. (Contributed by
NM, 17Mar1995.)

⊢ Rel 𝐴
& ⊢ Rel 𝐵
& ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵) ⇒ ⊢ 𝐴 = 𝐵 

Theorem  eqbrriv 4499* 
Inference from extensionality principle for relations. (Contributed by
NM, 12Dec2006.)

⊢ Rel 𝐴
& ⊢ Rel 𝐵
& ⊢ (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦) ⇒ ⊢ 𝐴 = 𝐵 

Theorem  eqrelrdv 4500* 
Deduce equality of relations from equivalence of membership.
(Contributed by Rodolfo Medina, 10Oct2010.)

⊢ Rel 𝐴
& ⊢ Rel 𝐵
& ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) 