Type  Label  Description 
Statement 

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

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (A × C) = (B ×
C)) 

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

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (C × A) = (C ×
B)) 

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

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

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

⊢ F/_xA & ⊢ F/_xB ⇒ ⊢ F/_x(A ×
B) 

Theorem  opelxp 4805 
Ordered pair membership in a cross product. (The proof was shortened by
Andrew Salmon, 12Aug2011.) (Contributed by NM, 15Nov1994.)
(Revised by set.mm contributors, 12Aug2011.)

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

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

⊢ (A(C × D)B ↔
(A ∈
C ∧
B ∈
D)) 

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

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

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

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

Theorem  fconstopab 4809* 
Representation of a constant function using ordered pairs. (Contributed
by NM, 12Oct1999.)

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

Theorem  vtoclr 4810* 
Variable to class conversion of transitive relation. (Contributed by
NM, 9Jun1998.)

⊢ ((xRy ∧ yRz) →
xRz) ⇒ ⊢ ((ARB ∧ BRC) →
ARC) 

Theorem  ralxp 4811* 
Universal quantification restricted to a cross product is equivalent to
a double restricted quantification. The hypothesis specifies an
implicit substitution. (Contributed by NM, 7Feb2004.) (Revised by
Mario Carneiro, 29Dec2014.)

⊢ (x = ⟨y, z⟩ → (φ ↔ ψ)) ⇒ ⊢ (∀x ∈ (A × B)φ ↔
∀y
∈ A
∀z
∈ B
ψ) 

Theorem  rexxp 4812* 
Existential quantification restricted to a cross product is equivalent
to a double restricted quantification. (Contributed by NM,
11Nov1995.) (Revised by Mario Carneiro, 14Feb2015.)

⊢ (x = ⟨y, z⟩ → (φ ↔ ψ)) ⇒ ⊢ (∃x ∈ (A × B)φ ↔
∃y
∈ A
∃z
∈ B
ψ) 

Theorem  ralxpf 4813* 
Version of ralxp 4811 with boundvariable hypotheses. (Contributed
by NM,
18Aug2006.) (Revised by set.mm contributors, 20Dec2008.)

⊢ Ⅎyφ
& ⊢ Ⅎzφ
& ⊢ Ⅎxψ
& ⊢ (x = ⟨y, z⟩ → (φ ↔ ψ)) ⇒ ⊢ (∀x ∈ (A × B)φ ↔
∀y
∈ A
∀z
∈ B
ψ) 

Theorem  rexxpf 4814* 
Version of rexxp 4812 with boundvariable hypotheses. (Contributed
by NM,
19Dec2008.)

⊢ Ⅎyφ
& ⊢ Ⅎzφ
& ⊢ Ⅎxψ
& ⊢ (x = ⟨y, z⟩ → (φ ↔ ψ)) ⇒ ⊢ (∃x ∈ (A × B)φ ↔
∃y
∈ A
∃z
∈ B
ψ) 

Theorem  iunxpf 4815* 
Indexed union on a cross product is equals a double indexed union. The
hypothesis specifies an implicit substitution. (Contributed by NM,
19Dec2008.)

⊢ F/_yC & ⊢ F/_zC & ⊢ F/_xD & ⊢ (x = ⟨y, z⟩ →
C = D) ⇒ ⊢ ∪x ∈ (A × B)C = ∪y ∈ A ∪z ∈ B D 

Theorem  brel 4816 
Two things in a binary relation belong to the relation's domain.
(Contributed by NM, 17May1996.)

⊢ R ⊆ (C ×
D) ⇒ ⊢ (ARB →
(A ∈
C ∧
B ∈
D)) 

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

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

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

⊢ (A ×
(B ∪ C)) = ((A
× B) ∪ (A × C)) 

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

⊢ ((A ∪
B) × C) = ((A
× C) ∪ (B × C)) 

Theorem  xpiundi 4820* 
Distributive law for cross product over indexed union. (Revised by
Mario Carneiro, 27Apr2014.) (Contributed by set.mm contributors,
27Apr2014.)

⊢ (C ×
∪x ∈ A B) = ∪x ∈ A (C ×
B) 

Theorem  xpiundir 4821* 
Distributive law for cross product over indexed union. (Revised by
Mario Carneiro, 27Apr2014.) (Contributed by set.mm contributors,
27Apr2014.)

⊢ (∪x ∈ A B ×
C) = ∪x ∈ A (B × C) 

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

⊢ ∪x ∈ A ({x} ×
B) = (A × B) 

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

⊢ ((A ∪
B) × (C ∪ D)) =
(((A × C) ∪ (A
× D)) ∪ ((B × C)
∪ (B × D))) 

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

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

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

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

Theorem  brinxp2 4826 
Intersection of binary relation with cross product. (Contributed by NM,
3Mar2007.)

⊢ (A(R ∩ (C
× D))B ↔ (A
∈ C
∧ B ∈ D ∧ ARB)) 

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

⊢ ((A ∈ C ∧ B ∈ D) →
(ARB ↔
A(R
∩ (C × D))B)) 

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

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

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

⊢ D =
(B × C)
& ⊢ (⟨x, y⟩ = A →
(φ ↔ ψ))
& ⊢ ((x ∈ B ∧ y ∈ C) →
φ) ⇒ ⊢ (A ∈ D →
ψ) 

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

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

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

⊢ R =
(D × F)
& ⊢ (⟨x, y⟩ = A →
(φ ↔ ψ))
& ⊢ (⟨z, w⟩ = B →
(ψ ↔ χ))
& ⊢ (⟨v, u⟩ = C →
(χ ↔ θ))
& ⊢ (((x ∈ D ∧ y ∈ F) ∧ (z ∈ D ∧ w ∈ F) ∧ (v ∈ D ∧ u ∈ F)) →
φ) ⇒ ⊢ ((A ∈ R ∧ B ∈ R ∧ C ∈ R) →
θ) 

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

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

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

⊢ (∅ ×
A) = ∅ 

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

⊢ (A =
B → (Rel A ↔ Rel B)) 

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

⊢ A =
B ⇒ ⊢ (Rel A
↔ Rel B) 

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

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (Rel A ↔ Rel B)) 

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

⊢ F/_xA ⇒ ⊢ ℲxRel
A 

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

⊢ (A ⊆ B →
(Rel B → Rel A)) 

Theorem  ssrel 4839* 
A subclass relationship depends only on a relation's ordered pairs.
Theorem 3.2(i) of [Monk1] p. 33. (The
proof was shortened by Andrew
Salmon, 27Aug2011.) (Contributed by NM, 2Aug1994.) (Revised by
set.mm contributors, 27Aug2011.)

⊢ (Rel A
→ (A ⊆ B ↔
∀x∀y(⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B))) 

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

⊢ ((Rel A
∧ Rel B)
→ (A = B ↔ ∀x∀y(⟨x, y⟩ ∈ A ↔
⟨x,
y⟩ ∈ B))) 

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

⊢ Rel A
& ⊢ (⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B) ⇒ ⊢ A ⊆ B 

Theorem  relssdv 4842* 
Deduction from subclass principle for relations. (Contributed by set.mm
contributors, 11Sep2004.)

⊢ (φ
→ Rel A) & ⊢ (φ
→ (⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B)) ⇒ ⊢ (φ
→ A ⊆ B) 

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

⊢ (⟨x, y⟩ ∈ A ↔ ⟨x, y⟩ ∈ B) ⇒ ⊢ ((Rel A
∧ Rel B)
→ A = B) 

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

⊢ Rel A
& ⊢ Rel B
& ⊢ (⟨x, y⟩ ∈ A ↔ ⟨x, y⟩ ∈ B) ⇒ ⊢ A =
B 

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

⊢ Rel A
& ⊢ Rel B
& ⊢ (xAy ↔
xBy) ⇒ ⊢ A =
B 

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

⊢ Rel A
& ⊢ Rel B
& ⊢ (φ
→ (⟨x, y⟩ ∈ A ↔ ⟨x, y⟩ ∈ B)) ⇒ ⊢ (φ
→ A = B) 

Theorem  eqrelrdv2 4847* 
A version of eqrelrdv 4846. (Contributed by Rodolfo Medina,
10Oct2010.)

⊢ (φ
→ (⟨x, y⟩ ∈ A ↔ ⟨x, y⟩ ∈ B)) ⇒ ⊢ (((Rel A
∧ Rel B)
∧ φ)
→ A = B) 

Theorem  ssrelrel 4848* 
A subclass relationship determined by ordered triples. Use relrelss 5130
to express the antecedent in terms of the relation predicate. (The
proof was shortened by Andrew Salmon, 27Aug2011.) (Contributed by NM,
17Dec2008.) (Revised by set.mm contributors, 27Aug2011.)

⊢ (A ⊆ ((V × V) × V) → (A ⊆ B ↔ ∀x∀y∀z(⟨⟨x, y⟩, z⟩ ∈ A → ⟨⟨x, y⟩, z⟩ ∈ B))) 

Theorem  eqrelrel 4849* 
Extensionality principle for ordered triples (used by 2place operations
dfoprab 5567), analogous to eqrel 4840. Use relrelss 5130 to express the
antecedent in terms of the relation predicate. (Contributed by NM,
17Dec2008.)

⊢ ((A ∪
B) ⊆
((V × V) × V) → (A =
B ↔ ∀x∀y∀z(⟨⟨x, y⟩, z⟩ ∈ A ↔ ⟨⟨x, y⟩, z⟩ ∈ B))) 

Theorem  elrel 4850* 
A member of a relation is an ordered pair. (Contributed by NM,
17Sep2006.)

⊢ ((Rel R
∧ A ∈ R) →
∃x∃y A = ⟨x, y⟩) 

Theorem  relsn 4851 
A singleton is a relation iff it is an ordered pair. (Contributed by
NM, 24Sep2013.)

⊢ A ∈ V ⇒ ⊢ (Rel {A}
↔ A ∈ (V × V)) 

Theorem  relsnop 4852 
A singleton of an ordered pair is a relation. (Contributed by NM,
17May1998.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ Rel {⟨A, B⟩} 

Theorem  xpss12 4853 
Subset theorem for cross product. Generalization of Theorem 101 of
[Suppes] p. 52. (The proof was shortened
by Andrew Salmon,
27Aug2011.) (Contributed by NM, 26Aug1995.) (Revised by set.mm
contributors, 27Aug2011.)

⊢ ((A ⊆ B ∧ C ⊆ D) →
(A × C) ⊆ (B × D)) 

Theorem  xpss 4854 
A cross product is included in the ordered pair universe. Exercise 3 of
[TakeutiZaring] p. 25.
(Contributed by NM, 2Aug1994.)

⊢ (A ×
B) ⊆ (V
× V) 

Theorem  relxp 4855 
A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37.
(Contributed by NM, 2Aug1994.)

⊢ Rel (A
× B) 

Theorem  xpss1 4856 
Subset relation for cross product. (Contributed by Jeff Hankins,
30Aug2009.)

⊢ (A ⊆ B →
(A × C) ⊆ (B × C)) 

Theorem  xpss2 4857 
Subset relation for cross product. (Contributed by Jeff Hankins,
30Aug2009.)

⊢ (A ⊆ B →
(C × A) ⊆ (C × B)) 

Theorem  br1st 4858* 
Binary relationship equivalence for the 1^{st} function.
(Contributed
by set.mm contributors, 8Jan2015.)

⊢ B ∈ V ⇒ ⊢ (A1^{st} B ↔ ∃x A = ⟨B, x⟩) 

Theorem  br2nd 4859* 
Binary relationship equivalence for the 2^{nd} function.
(Contributed
by set.mm contributors, 8Jan2015.)

⊢ B ∈ V ⇒ ⊢ (A2^{nd} B ↔ ∃x A = ⟨x, B⟩) 

Theorem  brswap2 4860 
Binary relationship equivalence for the Swap
function.
(Contributed by set.mm contributors, 8Jan2015.)

⊢ B ∈ V
& ⊢ C ∈ V ⇒ ⊢ (A Swap ⟨B, C⟩ ↔ A =
⟨C,
B⟩) 

Theorem  relun 4861 
The union of two relations is a relation. Compare Exercise 5 of
[TakeutiZaring] p. 25. (Contributed
by NM, 12Aug1994.)

⊢ (Rel (A
∪ B) ↔ (Rel A ∧ Rel B)) 

Theorem  relin1 4862 
The intersection with a relation is a relation. (Contributed by NM,
16Aug1994.)

⊢ (Rel A
→ Rel (A ∩ B)) 

Theorem  relin2 4863 
The intersection with a relation is a relation. (Contributed by NM,
17Jan2006.)

⊢ (Rel B
→ Rel (A ∩ B)) 

Theorem  reldif 4864 
A difference cutting down a relation is a relation. (Contributed by NM,
31Mar1998.)

⊢ (Rel A
→ Rel (A ∖ B)) 

Theorem  reliun 4865 
An indexed union is a relation iff each member of its indexed family is
a relation. (Contributed by set.mm contributors, 19Dec2008.)

⊢ (Rel ∪x ∈ A B ↔ ∀x ∈ A Rel
B) 

Theorem  reliin 4866 
An indexed intersection is a relation if if at least one of the member of
the indexed family is a relation. (Contributed by set.mm contributors,
8Mar2014.)

⊢ (∃x ∈ A Rel B →
Rel ∩x
∈ A
B) 

Theorem  reluni 4867* 
The union of a class is a relation iff any member is a relation.
Exercise 6 of [TakeutiZaring] p.
25 and its converse. (Contributed by
NM, 13Aug2004.)

⊢ (Rel ∪A ↔ ∀x ∈ A Rel
x) 

Theorem  relint 4868* 
The intersection of a class is a relation if at least one member is a
relation. (Contributed by NM, 8Mar2014.)

⊢ (∃x ∈ A Rel x →
Rel ∩A) 

Theorem  rel0 4869 
The empty set is a relation. (Contributed by NM, 26Apr1998.)

⊢ Rel ∅ 

Theorem  relopabi 4870 
A class of ordered pairs is a relation. (Contributed by Mario Carneiro,
21Dec2013.)

⊢ A = {⟨x, y⟩ ∣ φ} ⇒ ⊢ Rel A 

Theorem  relopab 4871 
A class of ordered pairs is a relation. (Unnecessary distinct variable
restrictions were removed by Alan Sare, 9Jul2013.) (The proof was
shortened by Mario Carneiro, 21Dec2013.) (Contributed by NM,
8Mar1995.) (Revised by set.mm contributors, 9Jul2013.)

⊢ Rel {⟨x, y⟩ ∣ φ} 

Theorem  reli 4872 
The identity relation is a relation. Part of Exercise 4.12(p) of
[Mendelson] p. 235. (Contributed by
NM, 26Apr1998.) (Revised by
set.mm contributors, 21Dec2013.)

⊢ Rel I 

Theorem  rele 4873 
The membership relation is a relation. (Contributed by NM,
26Apr1998.) (Revised by set.mm contributors, 21Dec2013.)

⊢ Rel E 

Theorem  opabid2 4874* 
A relation expressed as an ordered pair abstraction. (Contributed by
set.mm contributors, 11Dec2006.)

⊢ (Rel A
→ {⟨x, y⟩ ∣ ⟨x, y⟩ ∈ A} =
A) 

Theorem  inopab 4875* 
Intersection of two ordered pair class abstractions. (Contributed by
NM, 30Sep2002.)

⊢ ({⟨x, y⟩ ∣ φ} ∩ {⟨x, y⟩ ∣ ψ}) =
{⟨x,
y⟩ ∣ (φ
∧ ψ)} 

Theorem  inxp 4876 
The intersection of two cross products. Exercise 9 of [TakeutiZaring]
p. 25. (The proof was shortened by Andrew Salmon, 27Aug2011.)
(Contributed by NM, 3Aug1994.) (Revised by set.mm contributors,
27Aug2011.)

⊢ ((A ×
B) ∩ (C × D)) =
((A ∩ C) × (B
∩ D)) 

Theorem  xpindi 4877 
Distributive law for cross product over intersection. Theorem 102 of
[Suppes] p. 52. (Contributed by NM,
26Sep2004.)

⊢ (A ×
(B ∩ C)) = ((A
× B) ∩ (A × C)) 

Theorem  xpindir 4878 
Distributive law for cross product over intersection. Similar to
Theorem 102 of [Suppes] p. 52.
(Contributed by NM, 26Sep2004.)

⊢ ((A ∩
B) × C) = ((A
× C) ∩ (B × C)) 

Theorem  opabbi2dv 4879* 
Deduce equality of a relation and an orderedpair class builder.
Compare abbi2dv 2468. (Contributed by NM, 24Feb2014.)

⊢ Rel A
& ⊢ (φ
→ (⟨x, y⟩ ∈ A ↔ ψ)) ⇒ ⊢ (φ
→ A = {⟨x, y⟩ ∣ ψ}) 

Theorem  ideqg 4880 
For sets, the identity relation is the same as equality. (Contributed
by NM, 30Apr2004.) (Revised by set.mm contributors, 27Aug2011.)

⊢ (B ∈ V →
(A I B
↔ A = B)) 

Theorem  ideqg2 4881 
For sets, the identity relation is the same as equality. (Contributed
by SF, 8Jan2015.)

⊢ (A ∈ V →
(A I B
↔ A = B)) 

Theorem  ideq 4882 
For sets, the identity relation is the same as equality. (Contributed
by NM, 13Aug1995.) (Revised by set.mm contributors, 1Jun2008.)

⊢ B ∈ V ⇒ ⊢ (A I
B ↔ A = B) 

Theorem  ididg 4883 
A set is identical to itself. (The proof was shortened by Andrew
Salmon, 27Aug2011.) (Contributed by NM, 28May2008.) (Revised by
set.mm contributors, 27Aug2011.)

⊢ (A ∈ V →
A I A) 

Theorem  coss1 4884 
Subclass theorem for composition. (Contributed by FL, 30Dec2010.)

⊢ (A ⊆ B →
(A ∘
C) ⊆
(B ∘
C)) 

Theorem  coss2 4885 
Subclass theorem for composition. (Contributed by set.mm contributors,
5Apr2013.)

⊢ (A ⊆ B →
(C ∘
A) ⊆
(C ∘
B)) 

Theorem  coeq1 4886 
Equality theorem for composition of two classes. (Contributed by set.mm
contributors, 3Jan1997.)

⊢ (A =
B → (A ∘ C) = (B ∘ C)) 

Theorem  coeq2 4887 
Equality theorem for composition of two classes. (Contributed by set.mm
contributors, 3Jan1997.)

⊢ (A =
B → (C ∘ A) = (C ∘ B)) 

Theorem  coeq1i 4888 
Equality inference for composition of two classes. (Contributed by
set.mm contributors, 16Nov2000.)

⊢ A =
B ⇒ ⊢ (A ∘ C) =
(B ∘
C) 

Theorem  coeq2i 4889 
Equality inference for composition of two classes. (Contributed by
set.mm contributors, 16Nov2000.)

⊢ A =
B ⇒ ⊢ (C ∘ A) =
(C ∘
B) 

Theorem  coeq1d 4890 
Equality deduction for composition of two classes. (Contributed by
set.mm contributors, 16Nov2000.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (A ∘ C) =
(B ∘
C)) 

Theorem  coeq2d 4891 
Equality deduction for composition of two classes. (Contributed by
set.mm contributors, 16Nov2000.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (C ∘ A) =
(C ∘
B)) 

Theorem  coeq12i 4892 
Equality inference for composition of two classes. (Contributed by FL,
7Jun2012.)

⊢ A =
B
& ⊢ C =
D ⇒ ⊢ (A ∘ C) =
(B ∘
D) 

Theorem  coeq12d 4893 
Equality deduction for composition of two classes. (Contributed by FL,
7Jun2012.)

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

Theorem  nfco 4894 
Boundvariable hypothesis builder for function value. (Contributed by
NM, 1Sep1999.)

⊢ F/_xA & ⊢ F/_xB ⇒ ⊢ F/_x(A ∘ B) 

Theorem  brco 4895* 
Binary relation on a composition. (Contributed by set.mm contributors,
21Sep2004.)

⊢ (A(C ∘ D)B ↔
∃x(ADx ∧ xCB)) 

Theorem  opelco 4896* 
Ordered pair membership in a composition. (The proof was shortened by
Andrew Salmon, 27Aug2011.) (Contributed by set.mm contributors,
27Dec1996.) (Revised by set.mm contributors, 27Aug2011.)

⊢ (⟨A, B⟩ ∈ (C ∘ D) ↔ ∃x(ADx ∧ xCB)) 

Theorem  cnvss 4897 
Subset theorem for converse. (Contributed by set.mm contributors,
22Mar1998.)

⊢ (A ⊆ B →
^{◡}A
⊆ ^{◡}B) 

Theorem  cnveq 4898 
Equality theorem for converse. (Contributed by set.mm contributors,
13Aug1995.)

⊢ (A =
B → ^{◡}A =
^{◡}B) 

Theorem  cnveqi 4899 
Equality inference for converse. (Contributed by set.mm contributors,
23Dec2008.)

⊢ A =
B ⇒ ⊢ ^{◡}A =
^{◡}B 

Theorem  cnveqd 4900 
Equality deduction for converse. (Contributed by set.mm contributors,
6Dec2013.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ ^{◡}A = ^{◡}B) 