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	elxp 4801*	Membership in a cross product. (Contributed by NM, 4-Jul-1994.)
|- (A e. (B X. C) <-> E.xE.y(A = <.x, y>. /\ (x e. B /\ y e. C)))
Theorem	elxp2 4802*	Membership in a cross product. (Contributed by NM, 23-Feb-2004.)
|- (A e. (B X. C) <-> E.x e. B E.y e. C A = <.x, y>.)
Theorem	xpeq12 4803	Equality theorem for cross product. (Contributed by FL, 31-Aug-2009.)
|- ((A = B /\ C = D) -> (A X. C) = (B X. D))
Theorem	xpeq1i 4804	Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
|- A = B   =>   |- (A X. C) = (B X. C)
Theorem	xpeq2i 4805	Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
|- A = B   =>   |- (C X. A) = (C X. B)
Theorem	xpeq12i 4806	Equality inference for cross product. (Contributed by FL, 31-Aug-2009.)
|- A = B   &   |- C = D   =>   |- (A X. C) = (B X. D)
Theorem	xpeq1d 4807	Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- (ph -> A = B)   =>   |- (ph -> (A X. C) = (B X. C))
Theorem	xpeq2d 4808	Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- (ph -> A = B)   =>   |- (ph -> (C X. A) = (C X. B))
Theorem	xpeq12d 4809	Equality deduction for cross product. (Contributed by NM, 8-Dec-2013.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A X. C) = (B X. D))
Theorem	nfxp 4810	Bound-variable hypothesis builder for cross product. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_xA   &   |- F/_xB   =>   |- F/_x(A X. B)
Theorem	opelxp 4811	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>. e. (C X. D) <-> (A e. C /\ B e. D))
Theorem	brxp 4812	Binary relation on a cross product. (Contributed by NM, 22-Apr-2004.)
|- (A(C X. D)B <-> (A e. C /\ B e. D))
Theorem	csbxpg 4813	Distribute proper substitution through the cross product of two classes. (Contributed by Alan Sare, 10-Nov-2012.)
|- (A e. D -> [_A / x]_(B X. C) = ([_A / x]_B X. [_A / x]_C))
Theorem	rabxp 4814*	Membership in a class builder restricted to a cross product. (Contributed by NM, 20-Feb-2014.)
|- (x = <.y, z>. -> (ph <-> ps))   =>   |- {x e. (A X. B) | ph} = {<.y, z>. | (y e. A /\ z e. B /\ ps)}
Theorem	fconstopab 4815*	Representation of a constant function using ordered pairs. (Contributed by NM, 12-Oct-1999.)
|- (A X. {B}) = {<.x, y>. | (x e. A /\ y = B)}
Theorem	vtoclr 4816*	Variable to class conversion of transitive relation. (Contributed by NM, 9-Jun-1998.)
|- ((xRy /\ yRz) -> xRz)   =>   |- ((ARB /\ BRC) -> ARC)
Theorem	xpiundi 4817*	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. U_x e. A B) = U_x e. A (C X. B)
Theorem	xpiundir 4818*	Distributive law for cross product over indexed union. (Contributed by set.mm contributors, 26-Apr-2014.) (Revised by Mario Carneiro, 27-Apr-2014.)
|- (U_x e. A B X. C) = U_x e. A (B X. C)
Theorem	iunxpconst 4819*	Membership in a union of cross products when the second factor is constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- U_x e. A ({x} X. B) = (A X. B)
Theorem	opeliunxp 4820	Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
|- (<.x, C>. e. U_x e. A ({x} X. B) <-> (x e. A /\ C e. B))
Theorem	eliunxp 4821*	Membership in a union of Cartesian products. Analogue of elxp 4801 for nonconstant B(x). (Contributed by Mario Carneiro, 29-Dec-2014.)
|- (C e. U_x e. A ({x} X. B) <-> E.xE.y(C = <.x, y>. /\ (x e. A /\ y e. B)))
Theorem	opeliunxp2 4822*	Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 14-Feb-2015.)
|- (x = C -> B = E)   =>   |- (<.C, D>. e. U_x e. A ({x} X. B) <-> (C e. A /\ D e. 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, 29-Dec-2014.)
|- (x = <.y, z>. -> (ph <-> ps))   =>   |- (A.x e. U_ y e. A ({y} X. B)ph <-> A.y e. A A.z e. B ps)
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, 14-Feb-2015.)
|- (x = <.y, z>. -> (ph <-> ps))   =>   |- (E.x e. U_ y e. A ({y} X. B)ph <-> E.y e. A E.z e. B ps)
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, 7-Feb-2004.) (Revised by Mario Carneiro, 29-Dec-2014.)
|- (x = <.y, z>. -> (ph <-> ps))   =>   |- (A.x e. (A X. B)ph <-> A.y e. A A.z e. B ps)
Theorem	rexxp 4826*	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>. -> (ph <-> ps))   =>   |- (E.x e. (A X. B)ph <-> E.y e. A E.z e. B ps)
Theorem	ralxpf 4827*	Version of ralxp 4825 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by set.mm contributors, 20-Dec-2008.)
|- F/yph   &   |- F/zph   &   |- F/xps   &   |- (x = <.y, z>. -> (ph <-> ps))   =>   |- (A.x e. (A X. B)ph <-> A.y e. A A.z e. B ps)
Theorem	rexxpf 4828*	Version of rexxp 4826 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.)
|- F/yph   &   |- F/zph   &   |- F/xps   &   |- (x = <.y, z>. -> (ph <-> ps))   =>   |- (E.x e. (A X. B)ph <-> E.y e. A E.z e. B ps)
Theorem	iunxpf 4829*	Indexed union on a cross product is equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008.)
|- F/_yC   &   |- F/_zC   &   |- F/_xD   &   |- (x = <.y, z>. -> C = D)   =>   |- U_x e. (A X. B)C = U_y e. A U_z e. B D
Theorem	brel 4830	Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996.)
|- R C_ (C X. D)   =>   |- (ARB -> (A e. C /\ B e. D))
Theorem	elxp3 4831*	Membership in a cross product. (Contributed by NM, 5-Mar-1995.)
|- (A e. (B X. C) <-> E.xE.y(<.x, y>. = A /\ <.x, y>. e. (B X. C)))
Theorem	xpundi 4832	Distributive law for cross product over union. Theorem 103 of [Suppes] p. 52. (Contributed by NM, 12-Aug-2004.)
|- (A X. (B u. C)) = ((A X. B) u. (A X. C))
Theorem	xpundir 4833	Distributive law for cross product over union. Similar to Theorem 103 of [Suppes] p. 52. (Contributed by NM, 30-Sep-2002.)
|- ((A u. B) X. C) = ((A X. C) u. (B X. C))
Theorem	xpun 4834	The cross product of two unions. (Contributed by NM, 12-Aug-2004.)
|- ((A u. B) X. (C u. D)) = (((A X. C) u. (A X. D)) u. ((B X. C) u. (B X. D)))
Theorem	brinxp2 4835	Intersection of binary relation with cross product. (Contributed by NM, 3-Mar-2007.)
|- (A(R i^i (C X. D))B <-> (A e. C /\ B e. D /\ ARB))
Theorem	brinxp 4836	Intersection of binary relation with cross product. (Contributed by NM, 9-Mar-1997.)
|- ((A e. C /\ B e. D) -> (ARB <-> A(R i^i (C X. D))B))
Theorem	opabssxp 4837*	An abstraction relation is a subset of a related cross product. (Contributed by NM, 16-Jul-1995.)
|- {<.x, y>. | ((x e. A /\ y e. B) /\ ph)} C_ (A X. B)
Theorem	optocl 4838*	Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995.)
|- D = (B X. C)   &   |- (<.x, y>. = A -> (ph <-> ps))   &   |- ((x e. B /\ y e. C) -> ph)   =>   |- (A e. D -> ps)
Theorem	2optocl 4839*	Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
|- R = (C X. D)   &   |- (<.x, y>. = A -> (ph <-> ps))   &   |- (<.z, w>. = B -> (ps <-> ch))   &   |- (((x e. C /\ y e. D) /\ (z e. C /\ w e. D)) -> ph)   =>   |- ((A e. R /\ B e. R) -> ch)
Theorem	3optocl 4840*	Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
|- R = (D X. F)   &   |- (<.x, y>. = A -> (ph <-> ps))   &   |- (<.z, w>. = B -> (ps <-> ch))   &   |- (<.v, u>. = C -> (ch <-> th))   &   |- (((x e. D /\ y e. F) /\ (z e. D /\ w e. F) /\ (v e. D /\ u e. F)) -> ph)   =>   |- ((A e. R /\ B e. R /\ C e. R) -> th)
Theorem	opbrop 4841*	Ordered pair membership in a relation. Special case. (Contributed by NM, 5-Aug-1995.)
|- (((z = A /\ w = B) /\ (v = C /\ u = D)) -> (ph <-> ps))   &   |- R = {<.x, y>. | ((x e. (S X. S) /\ y e. (S X. S)) /\ E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ ph))}   =>   |- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> (<.A, B>.R<.C, D>. <-> ps))
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, 4-Jul-1994.)
|- ((/) X. A) = (/)
Theorem	xpvv 4843	The cross product of the universe with itself is the universe. (Contributed by Scott Fenton, 14-Apr-2021.)
|- (_V X. _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, 27-Aug-2011.) (Contributed by NM, 2-Aug-1994.) (Revised by set.mm contributors, 27-Aug-2011.)
|- (A C_ B <-> A.xA.y(<.x, y>. e. A -> <.x, y>. e. B))
Theorem	eqrel 4845*	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 <-> A.xA.y(<.x, y>. e. A <-> <.x, y>. e. B))
Theorem	ssopr 4846*	Subclass principle for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
|- (A C_ B <-> A.xA.yA.z(<.<.x, y>., z>. e. A -> <.<.x, y>., z>. e. B))
Theorem	eqopr 4847*	Extensionality principle for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
|- (A = B <-> A.xA.yA.z(<.<.x, y>., z>. e. A <-> <.<.x, y>., z>. e. B))
Theorem	relssi 4848*	Inference from subclass principle for relations. (Contributed by NM, 31-Mar-1998.) (Revised by Scott Fenton, 15-Apr-2021.)
|- (<.x, y>. e. A -> <.x, y>. e. B)   =>   |- A C_ B
Theorem	relssdv 4849*	Deduction from subclass principle for relations. (Contributed by set.mm contributors, 11-Sep-2004.) (Revised by Scott Fenton, 16-Apr-2021.)
|- (ph -> (<.x, y>. e. A -> <.x, y>. e. B))   =>   |- (ph -> A C_ B)
Theorem	eqrelriv 4850*	Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012.) (Revised by Scott Fenton, 16-Apr-2021.)
|- (<.x, y>. e. A <-> <.x, y>. e. B)   =>   |- A = B
Theorem	eqbrriv 4851*	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 4852*	Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010.) (Revised by Scott Fenton, 16-Apr-2021.)
|- (ph -> (<.x, y>. e. A <-> <.x, y>. e. B))   =>   |- (ph -> A = B)
Theorem	eqoprriv 4853*	Equality inference for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
|- (<.<.x, y>., z>. e. A <-> <.<.x, y>., z>. e. B)   =>   |- A = B
Theorem	eqoprrdv 4854*	Equality deduction for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
|- (ph -> (<.<.x, y>., z>. e. A <-> <.<.x, y>., z>. e. B))   =>   |- (ph -> 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, 27-Aug-2011.) (Contributed by NM, 26-Aug-1995.) (Revised by set.mm contributors, 27-Aug-2011.)
|- ((A C_ B /\ C C_ D) -> (A X. C) C_ (B X. D))
Theorem	xpss1 4856	Subset relation for cross product. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- (A C_ B -> (A X. C) C_ (B X. C))
Theorem	xpss2 4857	Subset relation for cross product. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- (A C_ B -> (C X. A) C_ (C X. B))
Theorem	br1st 4858*	Binary relationship equivalence for the 1st function. (Contributed by set.mm contributors, 8-Jan-2015.)
|- B e. _V   =>   |- (A1stB <-> E.x A = <.B, x>.)
Theorem	br2nd 4859*	Binary relationship equivalence for the 2nd function. (Contributed by set.mm contributors, 8-Jan-2015.)
|- B e. _V   =>   |- (A2ndB <-> E.x A = <.x, B>.)
Theorem	brswap2 4860	Binary relationship equivalence for the Swap function. (Contributed by set.mm contributors, 8-Jan-2015.)
|- B e. _V   &   |- C e. _V   =>   |- (A Swap <.B, C>. <-> A = <.C, B>.)
Theorem	opabid2 4861*	A relation expressed as an ordered pair abstraction. (Contributed by set.mm contributors, 11-Dec-2006.)
|- {<.x, y>. | <.x, y>. e. A} = A
Theorem	inopab 4862*	Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
|- ({<.x, y>. | ph} i^i {<.x, y>. | ps}) = {<.x, y>. | (ph /\ ps)}
Theorem	inxp 4863	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 X. B) i^i (C X. D)) = ((A i^i C) X. (B i^i D))
Theorem	xpindi 4864	Distributive law for cross product over intersection. Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
|- (A X. (B i^i C)) = ((A X. B) i^i (A X. C))
Theorem	xpindir 4865	Distributive law for cross product over intersection. Similar to Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
|- ((A i^i B) X. C) = ((A X. C) i^i (B X. C))
Theorem	opabbi2i 4866*	Equality of a class variable and an ordered pair abstractions (inference rule). Compare abbi2i 2464. (Contributed by Scott Fenton, 18-Apr-2021.)
|- (<.x, y>. e. A <-> ph)   =>   |- A = {<.x, y>. | ph}
Theorem	opabbi2dv 4867*	Deduce equality of a relation and an ordered-pair class builder. Compare abbi2dv 2468. (Contributed by NM, 24-Feb-2014.)
|- (ph -> (<.x, y>. e. A <-> ps))   =>   |- (ph -> A = {<.x, y>. | ps})
Theorem	ideqg 4868	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 e. V -> (A _I B <-> A = B))
Theorem	ideqg2 4869	For sets, the identity relation is the same as equality. (Contributed by SF, 8-Jan-2015.)
|- (A e. V -> (A _I B <-> A = B))
Theorem	ideq 4870	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 e. _V   =>   |- (A _I B <-> A = B)
Theorem	ididg 4871	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 e. V -> A _I A)
Theorem	coss1 4872	Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
|- (A C_ B -> (A o. C) C_ (B o. C))
Theorem	coss2 4873	Subclass theorem for composition. (Contributed by set.mm contributors, 5-Apr-2013.)
|- (A C_ B -> (C o. A) C_ (C o. B))
Theorem	coeq1 4874	Equality theorem for composition of two classes. (Contributed by set.mm contributors, 3-Jan-1997.)
|- (A = B -> (A o. C) = (B o. C))
Theorem	coeq2 4875	Equality theorem for composition of two classes. (Contributed by set.mm contributors, 3-Jan-1997.)
|- (A = B -> (C o. A) = (C o. B))
Theorem	coeq1i 4876	Equality inference for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
|- A = B   =>   |- (A o. C) = (B o. C)
Theorem	coeq2i 4877	Equality inference for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
|- A = B   =>   |- (C o. A) = (C o. B)
Theorem	coeq1d 4878	Equality deduction for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
|- (ph -> A = B)   =>   |- (ph -> (A o. C) = (B o. C))
Theorem	coeq2d 4879	Equality deduction for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
|- (ph -> A = B)   =>   |- (ph -> (C o. A) = (C o. B))
Theorem	coeq12i 4880	Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.)
|- A = B   &   |- C = D   =>   |- (A o. C) = (B o. D)
Theorem	coeq12d 4881	Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A o. C) = (B o. D))
Theorem	nfco 4882	Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.)
|- F/_xA   &   |- F/_xB   =>   |- F/_x(A o. B)
Theorem	brco 4883*	Binary relation on a composition. (Contributed by set.mm contributors, 21-Sep-2004.)
|- (A(C o. D)B <-> E.x(ADx /\ xCB))
Theorem	opelco 4884*	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>. e. (C o. D) <-> E.x(ADx /\ xCB))
Theorem	cnvss 4885	Subset theorem for converse. (Contributed by set.mm contributors, 22-Mar-1998.)
|- (A C_ B -> `'A C_ `'B)
Theorem	cnveq 4886	Equality theorem for converse. (Contributed by set.mm contributors, 13-Aug-1995.)
|- (A = B -> `'A = `'B)
Theorem	cnveqi 4887	Equality inference for converse. (Contributed by set.mm contributors, 23-Dec-2008.)
|- A = B   =>   |- `'A = `'B
Theorem	cnveqd 4888	Equality deduction for converse. (Contributed by set.mm contributors, 6-Dec-2013.)
|- (ph -> A = B)   =>   |- (ph -> `'A = `'B)
Theorem	elcnv 4889*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by set.mm contributors, 24-Mar-1998.)
|- (A e. `'R <-> E.xE.y(A = <.x, y>. /\ yRx))
Theorem	elcnv2 4890*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by set.mm contributors, 11-Aug-2004.)
|- (A e. `'R <-> E.xE.y(A = <.x, y>. /\ <.y, x>. e. R))
Theorem	nfcnv 4891	Bound-variable hypothesis builder for converse. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_xA   =>   |- F/_x`'A
Theorem	brcnv 4892	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 4893	Ordered-pair membership in converse. (Contributed by set.mm contributors, 13-Aug-1995.)
|- (<.A, B>. e. `'R <-> <.B, A>. e. R)
Theorem	cnvco 4894	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 o. B) = (`'B o. `'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, 11-Aug-2004.)
|- `'U.A = U_x e. A `'x
Theorem	elrn 4896*	Membership in a range. (Contributed by set.mm contributors, 2-Apr-2004.)
|- (A e. ran B <-> E.x xBA)
Theorem	elrn2 4897*	Membership in a range. (Contributed by set.mm contributors, 10-Jul-1994.)
|- (A e. ran B <-> E.x<.x, A>. e. B)
Theorem	eldm 4898*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by set.mm contributors, 2-Apr-2004.)
|- (A e. dom B <-> E.y ABy)
Theorem	eldm2 4899*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by set.mm contributors, 1-Aug-1994.)
|- (A e. dom B <-> E.y<.A, y>. e. B)
Theorem	dfdm2 4900*	Alternate definition of domain. (Contributed by set.mm contributors, 5-Feb-2015.)
|- dom A = {x | E.y xAy}