P. 70 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 6901-7000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eceq2 6901	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> [ C ] A = [ C ] B )
Theorem	elecg 6902	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ( A e. V /\ B e. W ) -> ( A e. [ B ] R <-> B R A ) )
Theorem	elec 6903	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.)
|- A e. _V   &    |- B e. _V   =>    |- ( A e. [ B ] R <-> B R A )
Theorem	relelec 6904	Membership in an equivalence class when R is a relation. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( Rel R -> ( A e. [ B ] R <-> B R A ) )
Theorem	ecss 6905	An equivalence class is a subset of the domain. (Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   =>    |- ( ph -> [ A ] R C_ X )
Theorem	ecdmn0 6906	A representative of a nonempty equivalence class belongs to the domain of the equivalence relation. (Contributed by NM, 15-Feb-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( A e. dom R <-> [ A ] R =/= (/) )
Theorem	ereldm 6907	Equality of equivalence classes implies equivalence of domain membership. (Contributed by NM, 28-Jan-1996.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> [ A ] R = [ B ] R )   =>    |- ( ph -> ( A e. X <-> B e. X ) )
Theorem	erth 6908	Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> A e. X )   =>    |- ( ph -> ( A R B <-> [ A ] R = [ B ] R ) )
Theorem	erth2 6909	Basic property of equivalence relations. Compare Theorem 73 of [Suppes] p. 82. Assumes membership of the second argument in the domain. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> B e. X )   =>    |- ( ph -> ( A R B <-> [ A ] R = [ B ] R ) )
Theorem	erthi 6910	Basic property of equivalence relations. Part of Lemma 3N of [Enderton] p. 57. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   =>    |- ( ph -> [ A ] R = [ B ] R )
Theorem	erdisj 6911	Equivalence classes do not overlap. In other words, two equivalence classes are either equal or disjoint. Theorem 74 of [Suppes] p. 83. (Contributed by NM, 15-Jun-2004.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( R Er X -> ( [ A ] R = [ B ] R \/ ( [ A ] R i^i [ B ] R ) = (/) ) )
Theorem	ecidsn 6912	An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.)
|- [ A ] _I = { A }
Theorem	qseq1 6913	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> ( A /. C ) = ( B /. C ) )
Theorem	qseq2 6914	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> ( C /. A ) = ( C /. B ) )
Theorem	elqsg 6915*	Closed form of elqs 6916. (Contributed by Rodolfo Medina, 12-Oct-2010.)
|- ( B e. V -> ( B e. ( A /. R ) <-> E. x e. A B = [ x ] R ) )
Theorem	elqs 6916*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|- B e. _V   =>    |- ( B e. ( A /. R ) <-> E. x e. A B = [ x ] R )
Theorem	elqsi 6917*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( B e. ( A /. R ) -> E. x e. A B = [ x ] R )
Theorem	ecelqsg 6918	Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( ( R e. V /\ B e. A ) -> [ B ] R e. ( A /. R ) )
Theorem	ecelqsi 6919	Membership of an equivalence class in a quotient set. (Contributed by NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- R e. _V   =>    |- ( B e. A -> [ B ] R e. ( A /. R ) )
Theorem	ecopqsi 6920	"Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996.)
|- R e. _V   &    |- S = ( ( A X. A ) /. R )   =>    |- ( ( B e. A /\ C e. A ) -> [ <. B , C >. ] R e. S )
Theorem	qsexg 6921	A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( A e. V -> ( A /. R ) e. _V )
Theorem	qsex 6922	A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|- A e. _V   =>    |- ( A /. R ) e. _V
Theorem	uniqs 6923	The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|- ( R e. V -> U. ( A /. R ) = ( R " A ) )
Theorem	qsss 6924	A quotient set is a set of subsets of the base set. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er A )   =>    |- ( ph -> ( A /. R ) C_ ~P A )
Theorem	uniqs2 6925	The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- ( ph -> R Er A )   &    |- ( ph -> R e. V )   =>    |- ( ph -> U. ( A /. R ) = A )
Theorem	snec 6926	The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- A e. _V   =>    |- { [ A ] R } = ( { A } /. R )
Theorem	ecqs 6927	Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.)
|- R e. _V   =>    |- [ A ] R = U. ( { A } /. R )
Theorem	ecid 6928	A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- A e. _V   =>    |- [ A ] `' _E = A
Theorem	qsid 6929	A set is equal to its quotient set mod converse epsilon. (Note: converse epsilon is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( A /. `' _E ) = A
Theorem	ectocld 6930*	Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- S = ( B /. R )   &    |- ( [ x ] R = A -> ( ph <-> ps ) )   &    |- ( ( ch /\ x e. B ) -> ph )   =>    |- ( ( ch /\ A e. S ) -> ps )
Theorem	ectocl 6931*	Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- S = ( B /. R )   &    |- ( [ x ] R = A -> ( ph <-> ps ) )   &    |- ( x e. B -> ph )   =>    |- ( A e. S -> ps )
Theorem	elqsn0 6932	A quotient set doesn't contain the empty set. (Contributed by NM, 24-Aug-1995.)
|- ( ( dom R = A /\ B e. ( A /. R ) ) -> B =/= (/) )
Theorem	ecelqsdm 6933	Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995.)
|- ( ( dom R = A /\ [ B ] R e. ( A /. R ) ) -> B e. A )
Theorem	xpider 6934	A square cross product is an equivalence relation (in general it's not a poset). (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( A X. A ) Er A
Theorem	iiner 6935*	The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> |^|_ x e. A R Er B )
Theorem	riiner 6936*	The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( A. x e. A R Er B -> ( ( B X. B ) i^i |^|_ x e. A R ) Er B )
Theorem	erinxp 6937	A restricted equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er A )   &    |- ( ph -> B C_ A )   =>    |- ( ph -> ( R i^i ( B X. B ) ) Er B )
Theorem	ecinxp 6938	Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- ( ( ( R " A ) C_ A /\ B e. A ) -> [ B ] R = [ B ] ( R i^i ( A X. A ) ) )
Theorem	qsinxp 6939	Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ( R " A ) C_ A -> ( A /. R ) = ( A /. ( R i^i ( A X. A ) ) ) )
Theorem	qsdisj 6940	Members of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010.) (Revised by Mario Carneiro, 11-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> B e. ( A /. R ) )   &    |- ( ph -> C e. ( A /. R ) )   =>    |- ( ph -> ( B = C \/ ( B i^i C ) = (/) ) )
Theorem	qsdisj2 6941*	A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016.)
|- ( R Er X -> Disj x e. ( A /. R ) x )
Theorem	qsel 6942	If an element of a quotient set contains a given element, it is equal to the equivalence class of the element. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( ( R Er X /\ B e. ( A /. R ) /\ C e. B ) -> B = [ C ] R )
Theorem	uniinqs 6943	Class union distributes over the intersection of two subclasses of a quotient space. Compare uniin 3995. (Contributed by FL, 25-May-2007.) (Proof shortened by Mario Carneiro, 11-Jul-2014.)
|- R Er X   =>    |- ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) -> U. ( B i^i C ) = ( U. B i^i U. C ) )
Theorem	qliftlem 6944*	F, a function lift, is a subset of R X. S. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ( ph /\ x e. X ) -> [ x ] R e. ( X /. R ) )
Theorem	qliftrel 6945*	F, a function lift, is a subset of R X. S. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ph -> F C_ ( ( X /. R ) X. Y ) )
Theorem	qliftel 6946*	Elementhood in the relation F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ph -> ( [ C ] R F D <-> E. x e. X ( C R x /\ D = A ) ) )
Theorem	qliftel1 6947*	Elementhood in the relation F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ( ph /\ x e. X ) -> [ x ] R F A )
Theorem	qliftfun 6948*	The function F is the unique function defined by F ` [ x ] = A, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   &    |- ( x = y -> A = B )   =>    |- ( ph -> ( Fun F <-> A. x A. y ( x R y -> A = B ) ) )
Theorem	qliftfund 6949*	The function F is the unique function defined by F ` [ x ] = A, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   &    |- ( x = y -> A = B )   &    |- ( ( ph /\ x R y ) -> A = B )   =>    |- ( ph -> Fun F )
Theorem	qliftfuns 6950*	The function F is the unique function defined by F ` [ x ] = A, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ph -> ( Fun F <-> A. y A. z ( y R z -> [_ y / x ]_ A = [_ z / x ]_ A ) ) )
Theorem	qliftf 6951*	The domain and range of the function F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ph -> ( Fun F <-> F : ( X /. R ) --> Y ) )
Theorem	qliftval 6952*	The value of the function F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   &    |- ( x = C -> A = B )   &    |- ( ph -> Fun F )   =>    |- ( ( ph /\ C e. X ) -> ( F ` [ C ] R ) = B )
Theorem	ecoptocl 6953*	Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995.)
|- S = ( ( B X. C ) /. R )   &    |- ( [ <. x , y >. ] R = A -> ( ph <-> ps ) )   &    |- ( ( x e. B /\ y e. C ) -> ph )   =>    |- ( A e. S -> ps )
Theorem	2ecoptocl 6954*	Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995.)
|- S = ( ( C X. D ) /. R )   &    |- ( [ <. x , y >. ] R = A -> ( ph <-> ps ) )   &    |- ( [ <. z , w >. ] R = B -> ( ps <-> ch ) )   &    |- ( ( ( x e. C /\ y e. D ) /\ ( z e. C /\ w e. D ) ) -> ph )   =>    |- ( ( A e. S /\ B e. S ) -> ch )
Theorem	3ecoptocl 6955*	Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995.)
|- S = ( ( D X. D ) /. R )   &    |- ( [ <. x , y >. ] R = A -> ( ph <-> ps ) )   &    |- ( [ <. z , w >. ] R = B -> ( ps <-> ch ) )   &    |- ( [ <. v , u >. ] R = C -> ( ch <-> th ) )   &    |- ( ( ( x e. D /\ y e. D ) /\ ( z e. D /\ w e. D ) /\ ( v e. D /\ u e. D ) ) -> ph )   =>    |- ( ( A e. S /\ B e. S /\ C e. S ) -> th )
Theorem	brecop 6956*	Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.)
|- .~ e. _V   &    |- .~ Er ( G X. G )   &    |- H = ( ( G X. G ) /. .~ )   &    |- .<_ = { <. x , y >. | ( ( x e. H /\ y e. H ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] .~ /\ y = [ <. v , u >. ] .~ ) /\ ph ) ) }   &    |- ( ( ( ( z e. G /\ w e. G ) /\ ( A e. G /\ B e. G ) ) /\ ( ( v e. G /\ u e. G ) /\ ( C e. G /\ D e. G ) ) ) -> ( ( [ <. z , w >. ] .~ = [ <. A , B >. ] .~ /\ [ <. v , u >. ] .~ = [ <. C , D >. ] .~ ) -> ( ph <-> ps ) ) )   =>    |- ( ( ( A e. G /\ B e. G ) /\ ( C e. G /\ D e. G ) ) -> ( [ <. A , B >. ] .~ .<_ [ <. C , D >. ] .~ <-> ps ) )
Theorem	brecop2 6957	Binary relation on a quotient set. Lemma for real number construction. Eliminates antecedent from last hypothesis. (Contributed by NM, 13-Feb-1996.)
|- .~ e. _V   &    |- dom .~ = ( G X. G )   &    |- H = ( ( G X. G ) /. .~ )   &    |- R C_ ( H X. H )   &    |- .<_ C_ ( G X. G )   &    |- -. (/) e. G   &    |- dom .+ = ( G X. G )   &    |- ( ( ( A e. G /\ B e. G ) /\ ( C e. G /\ D e. G ) ) -> ( [ <. A , B >. ] .~ R [ <. C , D >. ] .~ <-> ( A .+ D ) .<_ ( B .+ C ) ) )   =>    |- ( [ <. A , B >. ] .~ R [ <. C , D >. ] .~ <-> ( A .+ D ) .<_ ( B .+ C ) )
Theorem	eroveu 6958*	Lemma for erov 6960 and eroprf 6961. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- J = ( A /. R )   &    |- K = ( B /. S )   &    |- ( ph -> T e. Z )   &    |- ( ph -> R Er U )   &    |- ( ph -> S Er V )   &    |- ( ph -> T Er W )   &    |- ( ph -> A C_ U )   &    |- ( ph -> B C_ V )   &    |- ( ph -> C C_ W )   &    |- ( ph -> .+ : ( A X. B ) --> C )   &    |- ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( r R s /\ t S u ) -> ( r .+ t ) T ( s .+ u ) ) )   =>    |- ( ( ph /\ ( X e. J /\ Y e. K ) ) -> E! z E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )
Theorem	erovlem 6959*	Lemma for erov 6960 and eroprf 6961. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- J = ( A /. R )   &    |- K = ( B /. S )   &    |- ( ph -> T e. Z )   &    |- ( ph -> R Er U )   &    |- ( ph -> S Er V )   &    |- ( ph -> T Er W )   &    |- ( ph -> A C_ U )   &    |- ( ph -> B C_ V )   &    |- ( ph -> C C_ W )   &    |- ( ph -> .+ : ( A X. B ) --> C )   &    |- ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( r R s /\ t S u ) -> ( r .+ t ) T ( s .+ u ) ) )   &    |- .+^ = { <. <. x , y >. , z >. | E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) }   =>    |- ( ph -> .+^ = ( x e. J , y e. K |-> ( iota z E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) ) )
Theorem	erov 6960*	The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- J = ( A /. R )   &    |- K = ( B /. S )   &    |- ( ph -> T e. Z )   &    |- ( ph -> R Er U )   &    |- ( ph -> S Er V )   &    |- ( ph -> T Er W )   &    |- ( ph -> A C_ U )   &    |- ( ph -> B C_ V )   &    |- ( ph -> C C_ W )   &    |- ( ph -> .+ : ( A X. B ) --> C )   &    |- ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( r R s /\ t S u ) -> ( r .+ t ) T ( s .+ u ) ) )   &    |- .+^ = { <. <. x , y >. , z >. | E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) }   &    |- ( ph -> R e. X )   &    |- ( ph -> S e. Y )   =>    |- ( ( ph /\ P e. A /\ Q e. B ) -> ( [ P ] R .+^ [ Q ] S ) = [ ( P .+ Q ) ] T )
Theorem	eroprf 6961*	Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- J = ( A /. R )   &    |- K = ( B /. S )   &    |- ( ph -> T e. Z )   &    |- ( ph -> R Er U )   &    |- ( ph -> S Er V )   &    |- ( ph -> T Er W )   &    |- ( ph -> A C_ U )   &    |- ( ph -> B C_ V )   &    |- ( ph -> C C_ W )   &    |- ( ph -> .+ : ( A X. B ) --> C )   &    |- ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( r R s /\ t S u ) -> ( r .+ t ) T ( s .+ u ) ) )   &    |- .+^ = { <. <. x , y >. , z >. | E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) }   &    |- ( ph -> R e. X )   &    |- ( ph -> S e. Y )   &    |- L = ( C /. T )   =>    |- ( ph -> .+^ : ( J X. K ) --> L )
Theorem	erov2 6962*	The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- J = ( A /. .~ )   &    |- .+^ = { <. <. x , y >. , z >. | E. p e. A E. q e. A ( ( x = [ p ] .~ /\ y = [ q ] .~ ) /\ z = [ ( p .+ q ) ] .~ ) }   &    |- ( ph -> .~ e. X )   &    |- ( ph -> .~ Er U )   &    |- ( ph -> A C_ U )   &    |- ( ph -> .+ : ( A X. A ) --> A )   &    |- ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. A /\ u e. A ) ) ) -> ( ( r .~ s /\ t .~ u ) -> ( r .+ t ) .~ ( s .+ u ) ) )   =>    |- ( ( ph /\ P e. A /\ Q e. A ) -> ( [ P ] .~ .+^ [ Q ] .~ ) = [ ( P .+ Q ) ] .~ )
Theorem	eroprf2 6963*	Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- J = ( A /. .~ )   &    |- .+^ = { <. <. x , y >. , z >. | E. p e. A E. q e. A ( ( x = [ p ] .~ /\ y = [ q ] .~ ) /\ z = [ ( p .+ q ) ] .~ ) }   &    |- ( ph -> .~ e. X )   &    |- ( ph -> .~ Er U )   &    |- ( ph -> A C_ U )   &    |- ( ph -> .+ : ( A X. A ) --> A )   &    |- ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. A /\ u e. A ) ) ) -> ( ( r .~ s /\ t .~ u ) -> ( r .+ t ) .~ ( s .+ u ) ) )   =>    |- ( ph -> .+^ : ( J X. J ) --> J )
Theorem	ecopoveq 6964*	This is the first of several theorems about equivalence relations of the kind used in construction of fractions and signed reals, involving operations on equivalent classes of ordered pairs. This theorem expresses the relation .~ (specified by the hypothesis) in terms of its operation F. (Contributed by NM, 16-Aug-1995.)
|- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .+ u ) = ( w .+ v ) ) ) }   =>    |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. .~ <. C , D >. <-> ( A .+ D ) = ( B .+ C ) ) )
Theorem	ecopovsym 6965*	Assuming the operation F is commutative, show that the relation .~, specified by the first hypothesis, is symmetric. (Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .+ u ) = ( w .+ v ) ) ) }   &    |- ( x .+ y ) = ( y .+ x )   =>    |- ( A .~ B -> B .~ A )
Theorem	ecopovtrn 6966*	Assuming that operation F is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation .~, specified by the first hypothesis, is transitive. (Contributed by NM, 11-Feb-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .+ u ) = ( w .+ v ) ) ) }   &    |- ( x .+ y ) = ( y .+ x )   &    |- ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )   &    |- ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) )   &    |- ( ( x e. S /\ y e. S ) -> ( ( x .+ y ) = ( x .+ z ) -> y = z ) )   =>    |- ( ( A .~ B /\ B .~ C ) -> A .~ C )
Theorem	ecopover 6967*	Assuming that operation F is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation .~, specified by the first hypothesis, is an equivalence relation. (Contributed by NM, 16-Feb-1996.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .+ u ) = ( w .+ v ) ) ) }   &    |- ( x .+ y ) = ( y .+ x )   &    |- ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )   &    |- ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) )   &    |- ( ( x e. S /\ y e. S ) -> ( ( x .+ y ) = ( x .+ z ) -> y = z ) )   =>    |- .~ Er ( S X. S )
Theorem	eceqoveq 6968*	Equality of equivalence relation in terms of an operation. (Contributed by NM, 15-Feb-1996.) (Proof shortened by Mario Carneiro, 12-Aug-2015.)
|- .~ Er ( S X. S )   &    |- dom .+ = ( S X. S )   &    |- -. (/) e. S   &    |- ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )   &    |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. .~ <. C , D >. <-> ( A .+ D ) = ( B .+ C ) ) )   =>    |- ( ( A e. S /\ C e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) )
Theorem	th3qlem1 6969*	Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The third hypothesis is the compatibility assumption. (Contributed by NM, 3-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- .~ Er S   &    |- ( ( ( y e. S /\ w e. S ) /\ ( z e. S /\ v e. S ) ) -> ( ( y .~ w /\ z .~ v ) -> ( y .+ z ) .~ ( w .+ v ) ) )   =>    |- ( ( A e. ( S /. .~ ) /\ B e. ( S /. .~ ) ) -> E* x E. y E. z ( ( A = [ y ] .~ /\ B = [ z ] .~ ) /\ x = [ ( y .+ z ) ] .~ ) )
Theorem	th3qlem2 6970*	Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. The fourth hypothesis is the compatibility assumption. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- .~ e. _V   &    |- .~ Er ( S X. S )   &    |- ( ( ( ( w e. S /\ v e. S ) /\ ( u e. S /\ t e. S ) ) /\ ( ( s e. S /\ f e. S ) /\ ( g e. S /\ h e. S ) ) ) -> ( ( <. w , v >. .~ <. u , t >. /\ <. s , f >. .~ <. g , h >. ) -> ( <. w , v >. .+ <. s , f >. ) .~ ( <. u , t >. .+ <. g , h >. ) ) )   =>    |- ( ( A e. ( ( S X. S ) /. .~ ) /\ B e. ( ( S X. S ) /. .~ ) ) -> E* z E. w E. v E. u E. t ( ( A = [ <. w , v >. ] .~ /\ B = [ <. u , t >. ] .~ ) /\ z = [ ( <. w , v >. .+ <. u , t >. ) ] .~ ) )
Theorem	th3qcor 6971*	Corollary of Theorem 3Q of [Enderton] p. 60. (Contributed by NM, 12-Nov-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|- .~ e. _V   &    |- .~ Er ( S X. S )   &    |- ( ( ( ( w e. S /\ v e. S ) /\ ( u e. S /\ t e. S ) ) /\ ( ( s e. S /\ f e. S ) /\ ( g e. S /\ h e. S ) ) ) -> ( ( <. w , v >. .~ <. u , t >. /\ <. s , f >. .~ <. g , h >. ) -> ( <. w , v >. .+ <. s , f >. ) .~ ( <. u , t >. .+ <. g , h >. ) ) )   &    |- G = { <. <. x , y >. , z >. | ( ( x e. ( ( S X. S ) /. .~ ) /\ y e. ( ( S X. S ) /. .~ ) ) /\ E. w E. v E. u E. t ( ( x = [ <. w , v >. ] .~ /\ y = [ <. u , t >. ] .~ ) /\ z = [ ( <. w , v >. .+ <. u , t >. ) ] .~ ) ) }   =>    |- Fun G
Theorem	th3q 6972*	Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- .~ e. _V   &    |- .~ Er ( S X. S )   &    |- ( ( ( ( w e. S /\ v e. S ) /\ ( u e. S /\ t e. S ) ) /\ ( ( s e. S /\ f e. S ) /\ ( g e. S /\ h e. S ) ) ) -> ( ( <. w , v >. .~ <. u , t >. /\ <. s , f >. .~ <. g , h >. ) -> ( <. w , v >. .+ <. s , f >. ) .~ ( <. u , t >. .+ <. g , h >. ) ) )   &    |- G = { <. <. x , y >. , z >. | ( ( x e. ( ( S X. S ) /. .~ ) /\ y e. ( ( S X. S ) /. .~ ) ) /\ E. w E. v E. u E. t ( ( x = [ <. w , v >. ] .~ /\ y = [ <. u , t >. ] .~ ) /\ z = [ ( <. w , v >. .+ <. u , t >. ) ] .~ ) ) }   =>    |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( [ <. A , B >. ] .~ G [ <. C , D >. ] .~ ) = [ ( <. A , B >. .+ <. C , D >. ) ] .~ )
Theorem	ovec 6973*	Express an operation on equivalence classes of ordered pairs in terms of equivalence class of operations on ordered pairs. See set.mm for additional comments describing the hypotheses. (Unnecessary distinct variable restrictions were removed by David Abernethy, 4-Jun-2013.) (Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro, 4-Jun-2013.)
|- H e. _V   &    |- K e. _V   &    |- L e. _V   &    |- .~ e. _V   &    |- .~ Er ( S X. S )   &    |- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ph ) ) }   &    |- ( ( ( z = a /\ w = b ) /\ ( v = c /\ u = d ) ) -> ( ph <-> ps ) )   &    |- ( ( ( z = g /\ w = h ) /\ ( v = t /\ u = s ) ) -> ( ph <-> ch ) )   &    |- .+ = { <. <. x , y >. , z >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = J ) ) }   &    |- ( ( ( w = a /\ v = b ) /\ ( u = g /\ f = h ) ) -> J = K )   &    |- ( ( ( w = c /\ v = d ) /\ ( u = t /\ f = s ) ) -> J = L )   &    |- ( ( ( w = A /\ v = B ) /\ ( u = C /\ f = D ) ) -> J = H )   &    |- .+^ = { <. <. x , y >. , z >. | ( ( x e. Q /\ y e. Q ) /\ E. a E. b E. c E. d ( ( x = [ <. a , b >. ] .~ /\ y = [ <. c , d >. ] .~ ) /\ z = [ ( <. a , b >. .+ <. c , d >. ) ] .~ ) ) }   &    |- Q = ( ( S X. S ) /. .~ )   &    |- ( ( ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) /\ ( ( g e. S /\ h e. S ) /\ ( t e. S /\ s e. S ) ) ) -> ( ( ps /\ ch ) -> K .~ L ) )   =>    |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( [ <. A , B >. ] .~ .+^ [ <. C , D >. ] .~ ) = [ H ] .~ )
Theorem	ecovcom 6974*	Lemma used to transfer a commutative law via an equivalence relation. (Contributed by NM, 29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|- C = ( ( S X. S ) /. .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = [ <. D , G >. ] .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( x e. S /\ y e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. x , y >. ] .~ ) = [ <. H , J >. ] .~ )   &    |- D = H   &    |- G = J   =>    |- ( ( A e. C /\ B e. C ) -> ( A .+ B ) = ( B .+ A ) )
Theorem	ecovass 6975*	Lemma used to transfer an associative law via an equivalence relation. (Contributed by NM, 31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|- D = ( ( S X. S ) /. .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = [ <. G , H >. ] .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. N , Q >. ] .~ )   &    |- ( ( ( G e. S /\ H e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. G , H >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. J , K >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( N e. S /\ Q e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. N , Q >. ] .~ ) = [ <. L , M >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( G e. S /\ H e. S ) )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( N e. S /\ Q e. S ) )   &    |- J = L   &    |- K = M   =>    |- ( ( A e. D /\ B e. D /\ C e. D ) -> ( ( A .+ B ) .+ C ) = ( A .+ ( B .+ C ) ) )
Theorem	ecovdi 6976*	Lemma used to transfer a distributive law via an equivalence relation. (Contributed by NM, 2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|- D = ( ( S X. S ) /. .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. M , N >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( M e. S /\ N e. S ) ) -> ( [ <. x , y >. ] .~ .x. [ <. M , N >. ] .~ ) = [ <. H , J >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .x. [ <. z , w >. ] .~ ) = [ <. W , X >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. x , y >. ] .~ .x. [ <. v , u >. ] .~ ) = [ <. Y , Z >. ] .~ )   &    |- ( ( ( W e. S /\ X e. S ) /\ ( Y e. S /\ Z e. S ) ) -> ( [ <. W , X >. ] .~ .+ [ <. Y , Z >. ] .~ ) = [ <. K , L >. ] .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( M e. S /\ N e. S ) )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( W e. S /\ X e. S ) )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( v e. S /\ u e. S ) ) -> ( Y e. S /\ Z e. S ) )   &    |- H = K   &    |- J = L   =>    |- ( ( A e. D /\ B e. D /\ C e. D ) -> ( A .x. ( B .+ C ) ) = ( ( A .x. B ) .+ ( A .x. C ) ) )
2.4.29  The mapping operation
Syntax	cmap 6977	Extend the definition of a class to include the mapping operation. (Read for A ^m B, "the set of all functions that map from B to A.)
class ^m
Syntax	cpm 6978	Extend the definition of a class to include the partial mapping operation. (Read for A ^m B, "the set of all partial functions that map from B to A.)
class ^pm
Definition	df-map 6979*	Define the mapping operation or set exponentiation. The set of all functions that map from B to A is written ( A ^m B ) (see mapval 6989). Many authors write A followed by B as a superscript for this operation and rely on context to avoid confusion other exponentiation operations (e.g. Definition 10.42 of [TakeutiZaring] p. 95). Other authors show B as a prefixed superscript, which is read " A pre B " (e.g. definition of [Enderton] p. 52). Definition 8.21 of [Eisenberg] p. 125 uses the notation Map( B, A) for our ( A ^m B ). The up-arrow is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976). We adopt the first case of his notation (simple exponentiation) and subscript it with m to distinguish it from other kinds of exponentiation. (Contributed by NM, 8-Dec-2003.)
|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
Definition	df-pm 6980*	Define the partial mapping operation. A partial function from B to A is a function from a subset of B to A. The set of all partial functions from B to A is written ( A ^pm B ) (see pmvalg 6988). A notation for this operation apparently does not appear in the literature. We use ^pm to distinguish it from the less general set exponentiation operation ^m (df-map 6979) . See mapsspm 7006 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.)
|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
Theorem	mapprc 6981*	When A is a proper class, the class of all functions mapping A to B is empty. Exercise 4.41 of [Mendelson] p. 255. (Contributed by NM, 8-Dec-2003.)
|- ( -. A e. _V -> { f | f : A --> B } = (/) )
Theorem	pmex 6982*	The class of all partial functions from one set to another is a set. (Contributed by NM, 15-Nov-2007.)
|- ( ( A e. C /\ B e. D ) -> { f | ( Fun f /\ f C_ ( A X. B ) ) } e. _V )
Theorem	mapex 6983*	The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of [Kunen] p. 31. (Contributed by Raph Levien, 4-Dec-2003.)
|- ( ( A e. C /\ B e. D ) -> { f | f : A --> B } e. _V )
Theorem	fnmap 6984	Set exponentiation has a universal domain. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ^m Fn ( _V X. _V )
Theorem	fnpm 6985	Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- ^pm Fn ( _V X. _V )
Theorem	reldmmap 6986	Set exponentiation is a well-behaved binary operator. (Contributed by Stefan O'Rear, 27-Feb-2015.)
|- Rel dom ^m
Theorem	mapvalg 6987*	The value of set exponentiation. ( A ^m B ) is the set of all functions that map from B to A. Definition 10.24 of [Kunen] p. 24. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. C /\ B e. D ) -> ( A ^m B ) = { f | f : B --> A } )
Theorem	pmvalg 6988*	The value of the partial mapping operation. ( A ^pm B ) is the set of all partial functions that map from B to A. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. C /\ B e. D ) -> ( A ^pm B ) = { f e. ~P ( B X. A ) | Fun f } )
Theorem	mapval 6989*	The value of set exponentiation (inference version). ( A ^m B ) is the set of all functions that map from B to A. Definition 10.24 of [Kunen] p. 24. (Contributed by NM, 8-Dec-2003.)
|- A e. _V   &    |- B e. _V   =>    |- ( A ^m B ) = { f | f : B --> A }
Theorem	elmapg 6990	Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^m B ) <-> C : B --> A ) )
Theorem	elpmg 6991	The predicate "is a partial function." (Contributed by Mario Carneiro, 14-Nov-2013.)
|- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^pm B ) <-> ( Fun C /\ C C_ ( B X. A ) ) ) )
Theorem	elpm2g 6992	The predicate "is a partial function." (Contributed by NM, 31-Dec-2013.)
|- ( ( A e. V /\ B e. W ) -> ( F e. ( A ^pm B ) <-> ( F : dom F --> A /\ dom F C_ B ) ) )
Theorem	elpm2r 6993	Sufficient condition for being a partial function. (Contributed by NM, 31-Dec-2013.)
|- ( ( ( A e. V /\ B e. W ) /\ ( F : C --> A /\ C C_ B ) ) -> F e. ( A ^pm B ) )
Theorem	elpmi 6994	A partial function is a function. (Contributed by Mario Carneiro, 15-Sep-2015.)
|- ( F e. ( A ^pm B ) -> ( F : dom F --> A /\ dom F C_ B ) )
Theorem	pmfun 6995	A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( F e. ( A ^pm B ) -> Fun F )
Theorem	elmapex 6996	Eliminate antecedent for mapping theorems: domain can be taken to be a set. (Contributed by Stefan O'Rear, 8-Oct-2014.)
|- ( A e. ( B ^m C ) -> ( B e. _V /\ C e. _V ) )
Theorem	elmapi 6997	A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. ( B ^m C ) -> A : C --> B )
Theorem	fpmg 6998	A total function is a partial function. (Contributed by Mario Carneiro, 31-Dec-2013.)
|- ( ( A e. V /\ B e. W /\ F : A --> B ) -> F e. ( B ^pm A ) )
Theorem	pmss12g 6999	Subset relation for the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.)
|- ( ( ( A C_ C /\ B C_ D ) /\ ( C e. V /\ D e. W ) ) -> ( A ^pm B ) C_ ( C ^pm D ) )
Theorem	pmresg 7000	Elementhood of a restricted function in the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.)
|- ( ( B e. V /\ F e. ( A ^pm C ) ) -> ( F |` B ) e. ( A ^pm B ) )