P. 49 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 4801-4900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elxpi 4801*	Membership in a cross product. Uses fewer axioms than elxp 4802. (Contributed by NM, 4-Jul-1994.)
⊢ (A ∈ (B × C) → ∃x∃y(A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ C)))
Theorem	elxp 4802*	Membership in a cross product. (Contributed by NM, 4-Jul-1994.)
⊢ (A ∈ (B × C) ↔ ∃x∃y(A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ C)))
Theorem	elxp2 4803*	Membership in a cross product. (Contributed by NM, 23-Feb-2004.)
⊢ (A ∈ (B × C) ↔ ∃x ∈ B ∃y ∈ C A = ⟨x, y⟩)
Theorem	xpeq12 4804	Equality theorem for cross product. (Contributed by FL, 31-Aug-2009.)
⊢ ((A = B ∧ C = D) → (A × C) = (B × D))
Theorem	xpeq1i 4805	Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
⊢ A = B    ⇒   ⊢ (A × C) = (B × C)
Theorem	xpeq2i 4806	Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
⊢ A = B    ⇒   ⊢ (C × A) = (C × B)
Theorem	xpeq12i 4807	Equality inference for cross product. (Contributed by FL, 31-Aug-2009.)
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A × C) = (B × D)
Theorem	xpeq1d 4808	Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A × C) = (B × C))
Theorem	xpeq2d 4809	Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C × A) = (C × B))
Theorem	xpeq12d 4810	Equality deduction for cross product. (Contributed by NM, 8-Dec-2013.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A × C) = (B × D))
Theorem	nfxp 4811	Bound-variable hypothesis builder for cross product. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx(A × B)
Theorem	opelxp 4812	Ordered pair membership in a cross product. (The proof was shortened by Andrew Salmon, 12-Aug-2011.) (Contributed by NM, 15-Nov-1994.) (Revised by set.mm contributors, 12-Aug-2011.)
⊢ (⟨A, B⟩ ∈ (C × D) ↔ (A ∈ C ∧ B ∈ D))
Theorem	brxp 4813	Binary relation on a cross product. (Contributed by NM, 22-Apr-2004.)
⊢ (A(C × D)B ↔ (A ∈ C ∧ B ∈ D))
Theorem	csbxpg 4814	Distribute proper substitution through the cross product of two classes. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (A ∈ D → [A / x](B × C) = ([A / x]B × [A / x]C))
Theorem	rabxp 4815*	Membership in a class builder restricted to a cross product. (Contributed by NM, 20-Feb-2014.)
⊢ (x = ⟨y, z⟩ → (φ ↔ ψ))    ⇒   ⊢ {x ∈ (A × B) ∣ φ} = {⟨y, z⟩ ∣ (y ∈ A ∧ z ∈ B ∧ ψ)}
Theorem	fconstopab 4816*	Representation of a constant function using ordered pairs. (Contributed by NM, 12-Oct-1999.)
⊢ (A × {B}) = {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)}
Theorem	vtoclr 4817*	Variable to class conversion of transitive relation. (Contributed by NM, 9-Jun-1998.)
⊢ ((xRy ∧ yRz) → xRz)    ⇒   ⊢ ((ARB ∧ BRC) → ARC)
Theorem	xpiundi 4818*	Distributive law for cross product over indexed union. (Contributed by set.mm contributors, 26-Apr-2014.) (Revised by Mario Carneiro, 27-Apr-2014.)
⊢ (C × ∪x ∈ A B) = ∪x ∈ A (C × B)
Theorem	xpiundir 4819*	Distributive law for cross product over indexed union. (Contributed by set.mm contributors, 26-Apr-2014.) (Revised by Mario Carneiro, 27-Apr-2014.)
⊢ (∪x ∈ A B × C) = ∪x ∈ A (B × C)
Theorem	iunxpconst 4820*	Membership in a union of cross products when the second factor is constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ ∪x ∈ A ({x} × B) = (A × B)
Theorem	opeliunxp 4821	Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
⊢ (⟨x, C⟩ ∈ ∪x ∈ A ({x} × B) ↔ (x ∈ A ∧ C ∈ B))
Theorem	eliunxp 4822*	Membership in a union of Cartesian products. Analogue of elxp 4802 for nonconstant B(x). (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (C ∈ ∪x ∈ A ({x} × B) ↔ ∃x∃y(C = ⟨x, y⟩ ∧ (x ∈ A ∧ y ∈ B)))
Theorem	opeliunxp2 4823*	Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ (x = C → B = E)    ⇒   ⊢ (⟨C, D⟩ ∈ ∪x ∈ A ({x} × B) ↔ (C ∈ A ∧ D ∈ E))
Theorem	raliunxp 4824*	Write a double restricted quantification as one universal quantifier. In this version of ralxp 4826, B(y) is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (x = ⟨y, z⟩ → (φ ↔ ψ))    ⇒   ⊢ (∀x ∈ ∪ y ∈ A ({y} × B)φ ↔ ∀y ∈ A ∀z ∈ B ψ)
Theorem	rexiunxp 4825*	Write a double restricted quantification as one universal quantifier. In this version of rexxp 4827, B(y) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ (x = ⟨y, z⟩ → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ ∪ y ∈ A ({y} × B)φ ↔ ∃y ∈ A ∃z ∈ B ψ)
Theorem	ralxp 4826*	Universal quantification restricted to a Cartesian product is equivalent to a double restricted quantification. The hypothesis specifies an implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 29-Dec-2014.)
⊢ (x = ⟨y, z⟩ → (φ ↔ ψ))    ⇒   ⊢ (∀x ∈ (A × B)φ ↔ ∀y ∈ A ∀z ∈ B ψ)
Theorem	rexxp 4827*	Existential quantification restricted to a Cartesian product is equivalent to a double restricted quantification. (Contributed by NM, 11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.)
⊢ (x = ⟨y, z⟩ → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ (A × B)φ ↔ ∃y ∈ A ∃z ∈ B ψ)
Theorem	ralxpf 4828*	Version of ralxp 4826 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by set.mm contributors, 20-Dec-2008.)
⊢ Ⅎyφ    &   ⊢ Ⅎzφ    &   ⊢ Ⅎxψ    &   ⊢ (x = ⟨y, z⟩ → (φ ↔ ψ))    ⇒   ⊢ (∀x ∈ (A × B)φ ↔ ∀y ∈ A ∀z ∈ B ψ)
Theorem	rexxpf 4829*	Version of rexxp 4827 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.)
⊢ Ⅎyφ    &   ⊢ Ⅎzφ    &   ⊢ Ⅎxψ    &   ⊢ (x = ⟨y, z⟩ → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ (A × B)φ ↔ ∃y ∈ A ∃z ∈ B ψ)
Theorem	iunxpf 4830*	Indexed union on a cross product is equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008.)
⊢ ℲyC    &   ⊢ ℲzC    &   ⊢ ℲxD    &   ⊢ (x = ⟨y, z⟩ → C = D)    ⇒   ⊢ ∪x ∈ (A × B)C = ∪y ∈ A ∪z ∈ B D
Theorem	brel 4831	Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996.)
⊢ R ⊆ (C × D)    ⇒   ⊢ (ARB → (A ∈ C ∧ B ∈ D))
Theorem	elxp3 4832*	Membership in a cross product. (Contributed by NM, 5-Mar-1995.)
⊢ (A ∈ (B × C) ↔ ∃x∃y(⟨x, y⟩ = A ∧ ⟨x, y⟩ ∈ (B × C)))
Theorem	xpundi 4833	Distributive law for cross product over union. Theorem 103 of [Suppes] p. 52. (Contributed by NM, 12-Aug-2004.)
⊢ (A × (B ∪ C)) = ((A × B) ∪ (A × C))
Theorem	xpundir 4834	Distributive law for cross product over union. Similar to Theorem 103 of [Suppes] p. 52. (Contributed by NM, 30-Sep-2002.)
⊢ ((A ∪ B) × C) = ((A × C) ∪ (B × C))
Theorem	xpun 4835	The cross product of two unions. (Contributed by NM, 12-Aug-2004.)
⊢ ((A ∪ B) × (C ∪ D)) = (((A × C) ∪ (A × D)) ∪ ((B × C) ∪ (B × D)))
Theorem	brinxp2 4836	Intersection of binary relation with cross product. (Contributed by NM, 3-Mar-2007.)
⊢ (A(R ∩ (C × D))B ↔ (A ∈ C ∧ B ∈ D ∧ ARB))
Theorem	brinxp 4837	Intersection of binary relation with cross product. (Contributed by NM, 9-Mar-1997.)
⊢ ((A ∈ C ∧ B ∈ D) → (ARB ↔ A(R ∩ (C × D))B))
Theorem	opabssxp 4838*	An abstraction relation is a subset of a related cross product. (Contributed by NM, 16-Jul-1995.)
⊢ {⟨x, y⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} ⊆ (A × B)
Theorem	optocl 4839*	Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995.)
⊢ D = (B × C)    &   ⊢ (⟨x, y⟩ = A → (φ ↔ ψ))    &   ⊢ ((x ∈ B ∧ y ∈ C) → φ)    ⇒   ⊢ (A ∈ D → ψ)
Theorem	2optocl 4840*	Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
⊢ R = (C × D)    &   ⊢ (⟨x, y⟩ = A → (φ ↔ ψ))    &   ⊢ (⟨z, w⟩ = B → (ψ ↔ χ))    &   ⊢ (((x ∈ C ∧ y ∈ D) ∧ (z ∈ C ∧ w ∈ D)) → φ)    ⇒   ⊢ ((A ∈ R ∧ B ∈ R) → χ)
Theorem	3optocl 4841*	Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
⊢ 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 4842*	Ordered pair membership in a relation. Special case. (Contributed by NM, 5-Aug-1995.)
⊢ (((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 4843	The cross product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 4-Jul-1994.)
⊢ (∅ × A) = ∅
Theorem	xpvv 4844	The cross product of the universe with itself is the universe. (Contributed by Scott Fenton, 14-Apr-2021.)
⊢ (V × V) = V
Theorem	ssrel 4845*	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, 27-Aug-2011.) (Contributed by NM, 2-Aug-1994.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ (A ⊆ B ↔ ∀x∀y(⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B))
Theorem	eqrel 4846*	Extensionality principle for relations. Theorem 3.2(ii) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Revised by Scott Fenton, 14-Apr-2021.)
⊢ (A = B ↔ ∀x∀y(⟨x, y⟩ ∈ A ↔ ⟨x, y⟩ ∈ B))
Theorem	ssopr 4847*	Subclass principle for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ (A ⊆ B ↔ ∀x∀y∀z(⟨⟨x, y⟩, z⟩ ∈ A → ⟨⟨x, y⟩, z⟩ ∈ B))
Theorem	eqopr 4848*	Extensionality principle for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ (A = B ↔ ∀x∀y∀z(⟨⟨x, y⟩, z⟩ ∈ A ↔ ⟨⟨x, y⟩, z⟩ ∈ B))
Theorem	relssi 4849*	Inference from subclass principle for relations. (Contributed by NM, 31-Mar-1998.) (Revised by Scott Fenton, 15-Apr-2021.)
⊢ (⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B)    ⇒   ⊢ A ⊆ B
Theorem	relssdv 4850*	Deduction from subclass principle for relations. (Contributed by set.mm contributors, 11-Sep-2004.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ (φ → (⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B))    ⇒   ⊢ (φ → A ⊆ B)
Theorem	eqrelriv 4851*	Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ (⟨x, y⟩ ∈ A ↔ ⟨x, y⟩ ∈ B)    ⇒   ⊢ A = B
Theorem	eqbrriv 4852*	Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ (xAy ↔ xBy)    ⇒   ⊢ A = B
Theorem	eqrelrdv 4853*	Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ (φ → (⟨x, y⟩ ∈ A ↔ ⟨x, y⟩ ∈ B))    ⇒   ⊢ (φ → A = B)
Theorem	eqoprriv 4854*	Equality inference for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ (⟨⟨x, y⟩, z⟩ ∈ A ↔ ⟨⟨x, y⟩, z⟩ ∈ B)    ⇒   ⊢ A = B
Theorem	eqoprrdv 4855*	Equality deduction for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ (φ → (⟨⟨x, y⟩, z⟩ ∈ A ↔ ⟨⟨x, y⟩, z⟩ ∈ B))    ⇒   ⊢ (φ → A = B)
Theorem	xpss12 4856	Subset theorem for cross product. Generalization of Theorem 101 of [Suppes] p. 52. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by NM, 26-Aug-1995.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ ((A ⊆ B ∧ C ⊆ D) → (A × C) ⊆ (B × D))
Theorem	xpss1 4857	Subset relation for cross product. (Contributed by Jeff Hankins, 30-Aug-2009.)
⊢ (A ⊆ B → (A × C) ⊆ (B × C))
Theorem	xpss2 4858	Subset relation for cross product. (Contributed by Jeff Hankins, 30-Aug-2009.)
⊢ (A ⊆ B → (C × A) ⊆ (C × B))
Theorem	br1st 4859*	Binary relationship equivalence for the 1st function. (Contributed by set.mm contributors, 8-Jan-2015.)
⊢ B ∈ V    ⇒   ⊢ (A1st B ↔ ∃x A = ⟨B, x⟩)
Theorem	br2nd 4860*	Binary relationship equivalence for the 2nd function. (Contributed by set.mm contributors, 8-Jan-2015.)
⊢ B ∈ V    ⇒   ⊢ (A2nd B ↔ ∃x A = ⟨x, B⟩)
Theorem	brswap2 4861	Binary relationship equivalence for the Swap function. (Contributed by set.mm contributors, 8-Jan-2015.)
⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ (A Swap ⟨B, C⟩ ↔ A = ⟨C, B⟩)
Theorem	opabid2 4862*	A relation expressed as an ordered pair abstraction. (Contributed by set.mm contributors, 11-Dec-2006.)
⊢ {⟨x, y⟩ ∣ ⟨x, y⟩ ∈ A} = A
Theorem	inopab 4863*	Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
⊢ ({⟨x, y⟩ ∣ φ} ∩ {⟨x, y⟩ ∣ ψ}) = {⟨x, y⟩ ∣ (φ ∧ ψ)}
Theorem	inxp 4864	The intersection of two cross products. Exercise 9 of [TakeutiZaring] p. 25. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by NM, 3-Aug-1994.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ ((A × B) ∩ (C × D)) = ((A ∩ C) × (B ∩ D))
Theorem	xpindi 4865	Distributive law for cross product over intersection. Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
⊢ (A × (B ∩ C)) = ((A × B) ∩ (A × C))
Theorem	xpindir 4866	Distributive law for cross product over intersection. Similar to Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
⊢ ((A ∩ B) × C) = ((A × C) ∩ (B × C))
Theorem	opabbi2i 4867*	Equality of a class variable and an ordered pair abstractions (inference rule). Compare eqabi 2465. (Contributed by Scott Fenton, 18-Apr-2021.)
⊢ (⟨x, y⟩ ∈ A ↔ φ)    ⇒   ⊢ A = {⟨x, y⟩ ∣ φ}
Theorem	opabbi2dv 4868*	Deduce equality of a relation and an ordered-pair class builder. Compare eqabdv 2469. (Contributed by NM, 24-Feb-2014.)
⊢ (φ → (⟨x, y⟩ ∈ A ↔ ψ))    ⇒   ⊢ (φ → A = {⟨x, y⟩ ∣ ψ})
Theorem	ideqg 4869	For sets, the identity relation is the same as equality. (Contributed by NM, 30-Apr-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ (B ∈ V → (A I B ↔ A = B))
Theorem	ideqg2 4870	For sets, the identity relation is the same as equality. (Contributed by SF, 8-Jan-2015.)
⊢ (A ∈ V → (A I B ↔ A = B))
Theorem	ideq 4871	For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.) (Revised by set.mm contributors, 1-Jun-2008.)
⊢ B ∈ V    ⇒   ⊢ (A I B ↔ A = B)
Theorem	ididg 4872	A set is identical to itself. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by NM, 28-May-2008.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ (A ∈ V → A I A)
Theorem	coss1 4873	Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
⊢ (A ⊆ B → (A ∘ C) ⊆ (B ∘ C))
Theorem	coss2 4874	Subclass theorem for composition. (Contributed by set.mm contributors, 5-Apr-2013.)
⊢ (A ⊆ B → (C ∘ A) ⊆ (C ∘ B))
Theorem	coeq1 4875	Equality theorem for composition of two classes. (Contributed by set.mm contributors, 3-Jan-1997.)
⊢ (A = B → (A ∘ C) = (B ∘ C))
Theorem	coeq2 4876	Equality theorem for composition of two classes. (Contributed by set.mm contributors, 3-Jan-1997.)
⊢ (A = B → (C ∘ A) = (C ∘ B))
Theorem	coeq1i 4877	Equality inference for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
⊢ A = B    ⇒   ⊢ (A ∘ C) = (B ∘ C)
Theorem	coeq2i 4878	Equality inference for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
⊢ A = B    ⇒   ⊢ (C ∘ A) = (C ∘ B)
Theorem	coeq1d 4879	Equality deduction for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ∘ C) = (B ∘ C))
Theorem	coeq2d 4880	Equality deduction for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ∘ A) = (C ∘ B))
Theorem	coeq12i 4881	Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.)
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A ∘ C) = (B ∘ D)
Theorem	coeq12d 4882	Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A ∘ C) = (B ∘ D))
Theorem	nfco 4883	Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx(A ∘ B)
Theorem	brco 4884*	Binary relation on a composition. (Contributed by set.mm contributors, 21-Sep-2004.)
⊢ (A(C ∘ D)B ↔ ∃x(ADx ∧ xCB))
Theorem	opelco 4885*	Ordered pair membership in a composition. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 27-Dec-1996.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ (⟨A, B⟩ ∈ (C ∘ D) ↔ ∃x(ADx ∧ xCB))
Theorem	cnvss 4886	Subset theorem for converse. (Contributed by set.mm contributors, 22-Mar-1998.)
⊢ (A ⊆ B → ◡A ⊆ ◡B)
Theorem	cnveq 4887	Equality theorem for converse. (Contributed by set.mm contributors, 13-Aug-1995.)
⊢ (A = B → ◡A = ◡B)
Theorem	cnveqi 4888	Equality inference for converse. (Contributed by set.mm contributors, 23-Dec-2008.)
⊢ A = B    ⇒   ⊢ ◡A = ◡B
Theorem	cnveqd 4889	Equality deduction for converse. (Contributed by set.mm contributors, 6-Dec-2013.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → ◡A = ◡B)
Theorem	elcnv 4890*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by set.mm contributors, 24-Mar-1998.)
⊢ (A ∈ ◡R ↔ ∃x∃y(A = ⟨x, y⟩ ∧ yRx))
Theorem	elcnv2 4891*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by set.mm contributors, 11-Aug-2004.)
⊢ (A ∈ ◡R ↔ ∃x∃y(A = ⟨x, y⟩ ∧ ⟨y, x⟩ ∈ R))
Theorem	nfcnv 4892	Bound-variable hypothesis builder for converse. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ ℲxA    ⇒   ⊢ Ⅎx◡A
Theorem	brcnv 4893	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by set.mm contributors, 13-Aug-1995.)
⊢ (A◡RB ↔ BRA)
Theorem	opelcnv 4894	Ordered-pair membership in converse. (Contributed by set.mm contributors, 13-Aug-1995.)
⊢ (⟨A, B⟩ ∈ ◡R ↔ ⟨B, A⟩ ∈ R)
Theorem	cnvco 4895	Distributive law of converse over class composition. Theorem 26 of [Suppes] p. 64. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 19-Mar-1998.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ ◡(A ∘ B) = (◡B ∘ ◡A)
Theorem	cnvuni 4896*	The converse of a class union is the (indexed) union of the converses of its members. (Contributed by set.mm contributors, 11-Aug-2004.)
⊢ ◡∪A = ∪x ∈ A ◡x
Theorem	elrn 4897*	Membership in a range. (Contributed by set.mm contributors, 2-Apr-2004.)
⊢ (A ∈ ran B ↔ ∃x xBA)
Theorem	elrn2 4898*	Membership in a range. (Contributed by set.mm contributors, 10-Jul-1994.)
⊢ (A ∈ ran B ↔ ∃x⟨x, A⟩ ∈ B)
Theorem	eldm 4899*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by set.mm contributors, 2-Apr-2004.)
⊢ (A ∈ dom B ↔ ∃y ABy)
Theorem	eldm2 4900*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by set.mm contributors, 1-Aug-1994.)
⊢ (A ∈ dom B ↔ ∃y⟨A, y⟩ ∈ B)