P. 67 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6601-6700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	erth2 6601	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 6602	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	ecidsn 6603	An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.)
|- [ A ] _I = { A }
Theorem	qseq1 6604	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> ( A /. C ) = ( B /. C ) )
Theorem	qseq2 6605	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> ( C /. A ) = ( C /. B ) )
Theorem	elqsg 6606*	Closed form of elqs 6607. (Contributed by Rodolfo Medina, 12-Oct-2010.)
|- ( B e. V -> ( B e. ( A /. R ) <-> E. x e. A B = [ x ] R ) )
Theorem	elqs 6607*	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 6608*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( B e. ( A /. R ) -> E. x e. A B = [ x ] R )
Theorem	ecelqsg 6609	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 6610	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 6611	"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 6612	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 6613	A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|- A e. _V   =>    |- ( A /. R ) e. _V
Theorem	uniqs 6614	The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|- ( R e. V -> U. ( A /. R ) = ( R " A ) )
Theorem	qsss 6615	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 6616	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 6617	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 6618	Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.)
|- R e. _V   =>    |- [ A ] R = U. ( { A } /. R )
Theorem	ecid 6619	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	ecidg 6620	A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by Jim Kingdon, 8-Jan-2020.)
|- ( A e. V -> [ A ] `' _E = A )
Theorem	qsid 6621	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 6622*	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 6623*	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	elqsn0m 6624*	An element of a quotient set is inhabited. (Contributed by Jim Kingdon, 21-Aug-2019.)
|- ( ( dom R = A /\ B e. ( A /. R ) ) -> E. x x e. B )
Theorem	elqsn0 6625	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 6626	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 6627	A square Cartesian 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	iinerm 6628*	The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( ( E. y y e. A /\ A. x e. A R Er B ) -> |^|_ x e. A R Er B )
Theorem	riinerm 6629*	The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( ( E. y y e. A /\ A. x e. A R Er B ) -> ( ( B X. B ) i^i |^|_ x e. A R ) Er B )
Theorem	erinxp 6630	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 6631	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 6632	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	qsel 6633	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	qliftlem 6634*	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 6635*	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 6636*	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 6637*	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 6638*	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 6639*	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 6640*	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 6641*	The domain and codomain 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 6642*	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 6643*	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 6644*	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 6645*	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 6646*	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	eroveu 6647*	Lemma for eroprf 6649. (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 6648*	Lemma for eroprf 6649. (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	eroprf 6649*	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	eroprf2 6650*	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 6651*	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 6652*	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 6653*	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 6654*	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	ecopovsymg 6655*	Assuming the operation F is commutative, show that the relation .~, specified by the first hypothesis, is symmetric. (Contributed by Jim Kingdon, 1-Sep-2019.)
|- .~ = { <. 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 e. S /\ y e. S ) -> ( x .+ y ) = ( y .+ x ) )   =>    |- ( A .~ B -> B .~ A )
Theorem	ecopovtrng 6656*	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 Jim Kingdon, 1-Sep-2019.)
|- .~ = { <. 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 e. S /\ y e. S ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )   &    |- ( ( x e. S /\ y e. S /\ z e. S ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ( x e. S /\ y e. S /\ z e. S ) -> ( ( x .+ y ) = ( x .+ z ) -> y = z ) )   =>    |- ( ( A .~ B /\ B .~ C ) -> A .~ C )
Theorem	ecopoverg 6657*	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 Jim Kingdon, 1-Sep-2019.)
|- .~ = { <. 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 e. S /\ y e. S ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )   &    |- ( ( x e. S /\ y e. S /\ z e. S ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ( x e. S /\ y e. S /\ z e. S ) -> ( ( x .+ y ) = ( x .+ z ) -> y = z ) )   =>    |- .~ Er ( S X. S )
Theorem	th3qlem1 6658*	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 6659*	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 6660*	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 6661*	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	oviec 6662*	Express an operation on equivalence classes of ordered pairs in terms of equivalence class of operations on ordered pairs. See iset.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.)
|- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> H e. ( S X. S ) )   &    |- ( ( ( a e. S /\ b e. S ) /\ ( g e. S /\ h e. S ) ) -> K e. ( S X. S ) )   &    |- ( ( ( c e. S /\ d e. S ) /\ ( t e. S /\ s e. S ) ) -> L e. ( S X. S ) )   &    |- .~ 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 6663*	Lemma used to transfer a commutative law via an equivalence relation. Most uses will want ecovicom 6664 instead. (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	ecovicom 6664*	Lemma used to transfer a commutative law via an equivalence relation. (Contributed by Jim Kingdon, 15-Sep-2019.)
|- 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 >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> D = H )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> G = J )   =>    |- ( ( A e. C /\ B e. C ) -> ( A .+ B ) = ( B .+ A ) )
Theorem	ecovass 6665*	Lemma used to transfer an associative law via an equivalence relation. In most cases ecoviass 6666 will be more useful. (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	ecoviass 6666*	Lemma used to transfer an associative law via an equivalence relation. (Contributed by Jim Kingdon, 16-Sep-2019.)
|- 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 ) )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> J = L )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> K = M )   =>    |- ( ( A e. D /\ B e. D /\ C e. D ) -> ( ( A .+ B ) .+ C ) = ( A .+ ( B .+ C ) ) )
Theorem	ecovdi 6667*	Lemma used to transfer a distributive law via an equivalence relation. Most likely ecovidi 6668 will be more helpful. (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 ) ) )
Theorem	ecovidi 6668*	Lemma used to transfer a distributive law via an equivalence relation. (Contributed by Jim Kingdon, 17-Sep-2019.)
|- 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 ) )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> H = K )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> J = L )   =>    |- ( ( A e. D /\ B e. D /\ C e. D ) -> ( A .x. ( B .+ C ) ) = ( ( A .x. B ) .+ ( A .x. C ) ) )
2.6.26  The mapping operation
Syntax	cmap 6669	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 6670	Extend the definition of a class to include the partial mapping operation. (Read for A ^pm B, "the set of all partial functions that map from B to A.)
class ^pm
Definition	df-map 6671*	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 6681). 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 6672*	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 6680). 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 6671) . See mapsspm 6703 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 6673*	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 6674*	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 6675*	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 6676	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 6677	Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- ^pm Fn ( _V X. _V )
Theorem	reldmmap 6678	Set exponentiation is a well-behaved binary operator. (Contributed by Stefan O'Rear, 27-Feb-2015.)
|- Rel dom ^m
Theorem	mapvalg 6679*	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 6680*	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 6681*	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 6682	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	elmapd 6683	Deduction form of elmapg 6682. (Contributed by BJ, 11-Apr-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> ( C e. ( A ^m B ) <-> C : B --> A ) )
Theorem	mapdm0 6684	The empty set is the only map with empty domain. (Contributed by Glauco Siliprandi, 11-Oct-2020.) (Proof shortened by Thierry Arnoux, 3-Dec-2021.)
|- ( B e. V -> ( B ^m (/) ) = { (/) } )
Theorem	elpmg 6685	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 6686	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 6687	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 6688	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 6689	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 6690	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 6691	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	elmapfn 6692	A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019.)
|- ( A e. ( B ^m C ) -> A Fn C )
Theorem	elmapfun 6693	A mapping is always a function. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|- ( A e. ( B ^m C ) -> Fun A )
Theorem	elmapssres 6694	A restricted mapping is a mapping. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.)
|- ( ( A e. ( B ^m C ) /\ D C_ C ) -> ( A |` D ) e. ( B ^m D ) )
Theorem	fpmg 6695	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 6696	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 6697	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 ) )
Theorem	elmap 6698	Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.)
|- A e. _V   &    |- B e. _V   =>    |- ( F e. ( A ^m B ) <-> F : B --> A )
Theorem	mapval2 6699*	Alternate expression for the value of set exponentiation. (Contributed by NM, 3-Nov-2007.)
|- A e. _V   &    |- B e. _V   =>    |- ( A ^m B ) = ( ~P ( B X. A ) i^i { f | f Fn B } )
Theorem	elpm 6700	The predicate "is a partial function". (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
|- A e. _V   &    |- B e. _V   =>    |- ( F e. ( A ^pm B ) <-> ( Fun F /\ F C_ ( B X. A ) ) )