Type  Label  Description 
Statement 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ ℲxA & ⊢ ℲxB ⇒ ⊢ Ⅎx(A ×
B) 

Theorem  opelxp 4811 
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 4812 
Binary relation on a cross product. (Contributed by NM,
22Apr2004.)

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

Theorem  csbxpg 4813 
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 4814* 
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 4815* 
Representation of a constant function using ordered pairs. (Contributed
by NM, 12Oct1999.)

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

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

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

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

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

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

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

Theorem  iunxpconst 4819* 
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  opeliunxp 4820 
Membership in a union of Cartesian products. (Contributed by Mario
Carneiro, 29Dec2014.) (Revised by Mario Carneiro, 1Jan2017.)

⊢ (⟨x, C⟩ ∈ ∪x ∈ A ({x} × B)
↔ (x ∈ A ∧ C ∈ B)) 

Theorem  eliunxp 4821* 
Membership in a union of Cartesian products. Analogue of elxp 4801
for
nonconstant B(x). (Contributed by Mario Carneiro,
29Dec2014.)

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

Theorem  opeliunxp2 4822* 
Membership in a union of Cartesian products. (Contributed by Mario
Carneiro, 14Feb2015.)

⊢ (x =
C → B = E) ⇒ ⊢ (⟨C, D⟩ ∈ ∪x ∈ A ({x} × B)
↔ (C ∈ A ∧ D ∈ E)) 

Theorem  raliunxp 4823* 
Write a double restricted quantification as one universal quantifier.
In this version of ralxp 4825, B(y) is
not assumed to be constant.
(Contributed by Mario Carneiro, 29Dec2014.)

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

Theorem  rexiunxp 4824* 
Write a double restricted quantification as one universal quantifier.
In this version of rexxp 4826, B(y) is
not assumed to be constant.
(Contributed by Mario Carneiro, 14Feb2015.)

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

Theorem  ralxp 4825* 
Universal quantification restricted to a Cartesian 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 4826* 
Existential quantification restricted to a Cartesian 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 4827* 
Version of ralxp 4825 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 4828* 
Version of rexxp 4826 with boundvariable hypotheses. (Contributed
by NM,
19Dec2008.)

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

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

⊢ ℲyC & ⊢ ℲzC & ⊢ ℲxD & ⊢ (x = ⟨y, z⟩ →
C = D) ⇒ ⊢ ∪x ∈ (A × B)C = ∪y ∈ A ∪z ∈ B D 

Theorem  brel 4830 
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 4831* 
Membership in a cross product. (Contributed by NM, 5Mar1995.)

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

Theorem  xpundi 4832 
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 4833 
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  xpun 4834 
The cross product of two unions. (Contributed by NM, 12Aug2004.)

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

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

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

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

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

Theorem  opabssxp 4837* 
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 4838* 
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 4839* 
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 4840* 
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 4841* 
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 4842 
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  xpvv 4843 
The cross product of the universe with itself is the universe.
(Contributed by Scott Fenton, 14Apr2021.)

⊢ (V × V) = V 

Theorem  ssrel 4844* 
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.)

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

Theorem  eqrel 4845* 
Extensionality principle for relations. Theorem 3.2(ii) of [Monk1]
p. 33. (Contributed by NM, 2Aug1994.) (Revised by Scott Fenton,
14Apr2021.)

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

Theorem  ssopr 4846* 
Subclass principle for operators. (Contributed by Scott Fenton,
19Apr2021.)

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

Theorem  eqopr 4847* 
Extensionality principle for operators. (Contributed by Scott Fenton,
19Apr2021.)

⊢ (A =
B ↔ ∀x∀y∀z(⟨⟨x, y⟩, z⟩ ∈ A ↔ ⟨⟨x, y⟩, z⟩ ∈ B)) 

Theorem  relssi 4848* 
Inference from subclass principle for relations. (Contributed by NM,
31Mar1998.) (Revised by Scott Fenton, 15Apr2021.)

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

Theorem  relssdv 4849* 
Deduction from subclass principle for relations. (Contributed by set.mm
contributors, 11Sep2004.) (Revised by Scott Fenton, 16Apr2021.)

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

Theorem  eqrelriv 4850* 
Inference from extensionality principle for relations. (Contributed by
FL, 15Oct2012.) (Revised by Scott Fenton, 16Apr2021.)

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

Theorem  eqbrriv 4851* 
Inference from extensionality principle for relations. (Contributed by
NM, 12Dec2006.) (Revised by Scott Fenton, 16Apr2021.)

⊢ (xAy ↔
xBy) ⇒ ⊢ A =
B 

Theorem  eqrelrdv 4852* 
Deduce equality of relations from equivalence of membership.
(Contributed by Rodolfo Medina, 10Oct2010.) (Revised by Scott Fenton,
16Apr2021.)

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

Theorem  eqoprriv 4853* 
Equality inference for operators. (Contributed by Scott Fenton,
19Apr2021.)

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

Theorem  eqoprrdv 4854* 
Equality deduction for operators. (Contributed by Scott Fenton,
19Apr2021.)

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

Theorem  xpss12 4855 
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  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  opabid2 4861* 
A relation expressed as an ordered pair abstraction. (Contributed by
set.mm contributors, 11Dec2006.)

⊢ {⟨x, y⟩ ∣ ⟨x, y⟩ ∈ A} =
A 

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

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

Theorem  inxp 4863 
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 4864 
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 4865 
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  opabbi2i 4866* 
Equality of a class variable and an ordered pair abstractions
(inference rule). Compare abbi2i 2464. (Contributed by Scott Fenton,
18Apr2021.)

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

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

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

Theorem  ideqg 4868 
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 4869 
For sets, the identity relation is the same as equality. (Contributed
by SF, 8Jan2015.)

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

Theorem  ideq 4870 
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 4871 
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 4872 
Subclass theorem for composition. (Contributed by FL, 30Dec2010.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ ℲxA & ⊢ ℲxB ⇒ ⊢ Ⅎx(A ∘ B) 

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

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

Theorem  opelco 4884* 
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 4885 
Subset theorem for converse. (Contributed by set.mm contributors,
22Mar1998.)

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

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

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

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

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

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

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

Theorem  elcnv 4889* 
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by set.mm contributors, 24Mar1998.)

⊢ (A ∈ ^{◡}R
↔ ∃x∃y(A = ⟨x, y⟩ ∧ yRx)) 

Theorem  elcnv2 4890* 
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by set.mm contributors, 11Aug2004.)

⊢ (A ∈ ^{◡}R
↔ ∃x∃y(A = ⟨x, y⟩ ∧ ⟨y, x⟩ ∈ R)) 

Theorem  nfcnv 4891 
Boundvariable hypothesis builder for converse. (Contributed by NM,
31Jan2004.) (Revised by Mario Carneiro, 15Oct2016.)

⊢ ℲxA ⇒ ⊢ Ⅎx^{◡}A 

Theorem  brcnv 4892 
The converse of a binary relation swaps arguments. Theorem 11 of
[Suppes] p. 61. (Contributed by set.mm
contributors, 13Aug1995.)

⊢ (A^{◡}RB ↔
BRA) 

Theorem  opelcnv 4893 
Orderedpair membership in converse. (Contributed by set.mm
contributors, 13Aug1995.)

⊢ (⟨A, B⟩ ∈ ^{◡}R
↔ ⟨B, A⟩ ∈ R) 

Theorem  cnvco 4894 
Distributive law of converse over class composition. Theorem 26 of
[Suppes] p. 64. (The proof was shortened
by Andrew Salmon,
27Aug2011.) (Contributed by set.mm contributors, 19Mar1998.)
(Revised by set.mm contributors, 27Aug2011.)

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

Theorem  cnvuni 4895* 
The converse of a class union is the (indexed) union of the converses of
its members. (Contributed by set.mm contributors, 11Aug2004.)

⊢ ^{◡}∪A = ∪x ∈ A ^{◡}x 

Theorem  elrn 4896* 
Membership in a range. (Contributed by set.mm contributors,
2Apr2004.)

⊢ (A ∈ ran B ↔
∃x
xBA) 

Theorem  elrn2 4897* 
Membership in a range. (Contributed by set.mm contributors,
10Jul1994.)

⊢ (A ∈ ran B ↔
∃x⟨x, A⟩ ∈ B) 

Theorem  eldm 4898* 
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
set.mm contributors, 2Apr2004.)

⊢ (A ∈ dom B ↔
∃y
ABy) 

Theorem  eldm2 4899* 
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
set.mm contributors, 1Aug1994.)

⊢ (A ∈ dom B ↔
∃y⟨A, y⟩ ∈ B) 

Theorem  dfdm2 4900* 
Alternate definition of domain. (Contributed by set.mm contributors,
5Feb2015.)

⊢ dom A =
{x ∣
∃y
xAy} 