P. 240 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 - 23901-24000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xfree2 23901	A partial converse to 19.9t 1789. (Contributed by Stefan Allan, 21-Dec-2008.)
|- ( A. x ( ph -> A. x ph ) <-> A. x ( -. ph -> A. x -. ph ) )
Theorem	addltmulALT 23902	A proof readability experiment for addltmul 10159. (Contributed by Stefan Allan, 30-Oct-2010.) (Proof modification is discouraged.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 2 < A /\ 2 < B ) ) -> ( A + B ) < ( A x. B ) )
19.3  Mathbox for Thierry Arnoux
19.3.1  Propositional Calculus - misc additions
Theorem	bian1d 23903	Adding a superfluous conjunct in a biconditionnal. (Contributed by Thierry Arnoux, 26-Feb-2017.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ph -> ( ( ch /\ ps ) <-> ( ch /\ th ) ) )
Theorem	or3di 23904	Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.)
|- ( ( ph \/ ( ps /\ ch /\ ta ) ) <-> ( ( ph \/ ps ) /\ ( ph \/ ch ) /\ ( ph \/ ta ) ) )
Theorem	or3dir 23905	Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.)
|- ( ( ( ph /\ ps /\ ch ) \/ ta ) <-> ( ( ph \/ ta ) /\ ( ps \/ ta ) /\ ( ch \/ ta ) ) )
Theorem	3o1cs 23906	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
|- ( ( ph \/ ps \/ ch ) -> th )   =>    |- ( ph -> th )
Theorem	3o2cs 23907	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
|- ( ( ph \/ ps \/ ch ) -> th )   =>    |- ( ps -> th )
Theorem	3o3cs 23908	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
|- ( ( ph \/ ps \/ ch ) -> th )   =>    |- ( ch -> th )
Theorem	adantl3r 23909	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( ( ( ph /\ rh ) /\ mu ) /\ la ) -> ka )   =>    |- ( ( ( ( ( ph /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )
Theorem	adantl4r 23910	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( ( ( ( ph /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )   =>    |- ( ( ( ( ( ( ph /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )
Theorem	adantl5r 23911	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( ( ( ( ( ph /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )   =>    |- ( ( ( ( ( ( ( ph /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )
Theorem	adantl6r 23912	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( ( ( ( ( ( ph /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )   =>    |- ( ( ( ( ( ( ( ( ph /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) -> ka )
19.3.2  Predicate Calculus
19.3.2.1  Predicate Calculus - misc additions
Theorem	abeq2f 23913	Equality of a class variable and a class abstraction. In this version, the fact that x is a non-free variable in A is explicitely stated as a hypothesis. (Contributed by Thierry Arnoux, 11-May-2017.)
|- F/_ x A   =>    |- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) )
Theorem	eqvincg 23914*	A variable introduction law for class equality, deduction version. (Contributed by Thierry Arnoux, 2-Mar-2017.)
|- ( A e. V -> ( A = B <-> E. x ( x = A /\ x = B ) ) )
19.3.2.2  Restricted quantification - misc additions
Theorem	reximddv 23915*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> E. x e. A ch )
Theorem	raleqbid 23916	Equality deduction for restricted universal quantifier. (Contributed by Thierry Arnoux, 8-Mar-2017.)
|- F/ x ph   &    |- F/_ x A   &    |- F/_ x B   &    |- ( ph -> A = B )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )
Theorem	rexeqbid 23917	Equality deduction for restricted existential quantifier. (Contributed by Thierry Arnoux, 8-Mar-2017.)
|- F/ x ph   &    |- F/_ x A   &    |- F/_ x B   &    |- ( ph -> A = B )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) )
Theorem	ralcom4f 23918*	Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Revised by Thierry Arnoux, 8-Mar-2017.)
|- F/_ y A   =>    |- ( A. x e. A A. y ph <-> A. y A. x e. A ph )
Theorem	rexcom4f 23919*	Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Revised by Thierry Arnoux, 8-Mar-2017.)
|- F/_ y A   =>    |- ( E. x e. A E. y ph <-> E. y E. x e. A ph )
Theorem	rabid2f 23920	An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.)
|- F/_ x A   =>    |- ( A = { x e. A | ph } <-> A. x e. A ph )
Theorem	19.9d2rf 23921	A deduction version of one direction of 19.9 1793 with two variables (Contributed by Thierry Arnoux, 20-Mar-2017.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   &    |- ( ph -> F/ y ps )   &    |- ( ph -> E. x e. A E. y e. B ps )   =>    |- ( ph -> ps )
Theorem	19.9d2r 23922*	A deduction version of one direction of 19.9 1793 with two variables (Contributed by Thierry Arnoux, 30-Jan-2017.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ y ps )   &    |- ( ph -> E. x e. A E. y e. B ps )   =>    |- ( ph -> ps )
Theorem	r19.41vv 23923*	Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90. Version with two quantifiers (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( E. x e. A E. y e. B ( ph /\ ps ) <-> ( E. x e. A E. y e. B ph /\ ps ) )
19.3.2.3  Substitution (without distinct variables) - misc additions
Theorem	clelsb3f 23924	Substitution applied to an atomic wff (class version of elsb3 2152). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.)
|- F/_ y A   =>    |- ( [ x / y ] y e. A <-> x e. A )
19.3.2.4  Existential "at most one" - misc additions
Theorem	mo5f 23925*	Alternate definition of "at most one." (Contributed by Thierry Arnoux, 1-Mar-2017.)
|- F/ i ph   &    |- F/ j ph   =>    |- ( E* x ph <-> A. i A. j ( ( [ i / x ] ph /\ [ j / x ] ph ) -> i = j ) )
Theorem	nmo 23926*	Negation of "at most one". (Contributed by Thierry Arnoux, 26-Feb-2017.)
|- F/ y ph   =>    |- ( -. E* x ph <-> A. y E. x ( ph /\ x =/= y ) )
Theorem	moimd 23927*	"At most one" is preserved through implication (notice wff reversal). (Contributed by Thierry Arnoux, 25-Feb-2017.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E* x ch -> E* x ps ) )
19.3.2.5  Existential uniqueness - misc additions
Theorem	2reuswap2 23928*	A condition allowing swap of uniqueness and existential quantifiers. (Contributed by Thierry Arnoux, 7-Apr-2017.)
|- ( A. x e. A E* y ( y e. B /\ ph ) -> ( E! x e. A E. y e. B ph -> E! y e. B E. x e. A ph ) )
Theorem	reuxfr3d 23929*	Transfer existential uniqueness from a variable x to another variable y contained in expression A. Cf. reuxfr2d 4705 (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.)
|- ( ( ph /\ y e. C ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E* y e. C x = A )   =>    |- ( ph -> ( E! x e. B E. y e. C ( x = A /\ ps ) <-> E! y e. C ps ) )
Theorem	reuxfr4d 23930*	Transfer existential uniqueness from a variable x to another variable y contained in expression A. Cf. reuxfrd 4707 (Contributed by Thierry Arnoux, 7-Apr-2017.)
|- ( ( ph /\ y e. C ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E! y e. C x = A )   &    |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x e. B ps <-> E! y e. C ch ) )
Theorem	rexunirn 23931*	Restricted existential quantification over the union of the range of a function. Cf. rexrn 5831 and eluni2 3979. (Contributed by Thierry Arnoux, 19-Sep-2017.)
|- F = ( x e. A |-> B )   &    |- ( x e. A -> B e. V )   =>    |- ( E. x e. A E. y e. B ph -> E. y e. U. ran F ph )
19.3.2.6  Restricted "at most one" - misc additions
Theorem	rmoxfrdOLD 23932*	Transfer "at most one" restricted quantification from a variable x to another variable y contained in expression A. (Contributed by Thierry Arnoux, 7-Apr-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ph /\ y e. C ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E! y e. C x = A )   &    |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E* x ( x e. B /\ ps ) <-> E* y ( y e. C /\ ch ) ) )
Theorem	rmoxfrd 23933*	Transfer "at most one" restricted quantification from a variable x to another variable y contained in expression A. (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.)
|- ( ( ph /\ y e. C ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E! y e. C x = A )   &    |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E* x e. B ps <-> E* y e. C ch ) )
Theorem	ssrmo 23934	"At most one" existential quantification restricted to a subclass. (Contributed by Thierry Arnoux, 8-Oct-2017.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A C_ B -> ( E* x e. B ph -> E* x e. A ph ) )
Theorem	rmo3f 23935*	Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.)
|- F/_ x A   &    |- F/_ y A   &    |- F/ y ph   =>    |- ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) )
Theorem	rmo4fOLD 23936*	Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by Thierry Arnoux, 11-Oct-2016.) (Revised by Thierry Arnoux, 8-Mar-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/_ x A   &    |- F/_ y A   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E* x ( x e. A /\ ph ) <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )
Theorem	rmo4f 23937*	Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by Thierry Arnoux, 11-Oct-2016.) (Revised by Thierry Arnoux, 8-Mar-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.)
|- F/_ x A   &    |- F/_ y A   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )
19.3.3  General Set Theory
19.3.3.1  Class abstractions (a.k.a. class builders)
Theorem	ceqsexv2d 23938*	Elimination of an existential quantifier, using implicit substitution. (Contributed by Thierry Arnoux, 10-Sep-2016.)
|- A e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ps   =>    |- E. x ph
Theorem	rabbidva2 23939*	Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.)
|- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ch } )
Theorem	rabexgfGS 23940	Separation Scheme in terms of a restricted class abstraction. To be removed in profit of Glauco's equivalent version. (Contributed by Thierry Arnoux, 11-May-2017.)
|- F/_ x A   =>    |- ( A e. V -> { x e. A | ph } e. _V )
19.3.3.2  Image Sets
Theorem	abrexdomjm 23941*	An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( y e. A -> E* x ph )   =>    |- ( A e. V -> { x | E. y e. A ph } ~<_ A )
Theorem	abrexdom2jm 23942*	An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A e. V -> { x | E. y e. A x = B } ~<_ A )
Theorem	abrexexd 23943*	Existence of a class abstraction of existentially restricted sets. (Contributed by Thierry Arnoux, 10-May-2017.)
|- F/_ x A   &    |- ( ph -> A e. _V )   =>    |- ( ph -> { y | E. x e. A y = B } e. _V )
Theorem	elabreximd 23944*	Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.)
|- F/ x ph   &    |- F/ x ch   &    |- ( A = B -> ( ch <-> ps ) )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. C ) -> ps )   =>    |- ( ( ph /\ A e. { y | E. x e. C y = B } ) -> ch )
Theorem	elabreximdv 23945*	Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.)
|- ( A = B -> ( ch <-> ps ) )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. C ) -> ps )   =>    |- ( ( ph /\ A e. { y | E. x e. C y = B } ) -> ch )
Theorem	abrexss 23946*	A necessary condition for an image set to be a subset. (Contributed by Thierry Arnoux, 6-Feb-2017.)
|- F/_ x C   =>    |- ( A. x e. A B e. C -> { y | E. x e. A y = B } C_ C )
19.3.3.3  Set relations and operations - misc additions
Theorem	eqri 23947	Infer equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 7-Oct-2017.)
|- F/_ x A   &    |- F/_ x B   &    |- ( x e. A <-> x e. B )   =>    |- A = B
Theorem	rabss3d 23948*	Subclass law for restricted abstraction. (Contributed by Thierry Arnoux, 25-Sep-2017.)
|- ( ( ph /\ ( x e. A /\ ps ) ) -> x e. B )   =>    |- ( ph -> { x e. A | ps } C_ { x e. B | ps } )
Theorem	inin 23949	Intersection with an intersection (Contributed by Thierry Arnoux, 27-Dec-2016.)
|- ( A i^i ( A i^i B ) ) = ( A i^i B )
Theorem	difneqnul 23950	If the difference of two sets is not empty, then the sets are not equal. (Contributed by Thierry Arnoux, 28-Feb-2017.)
|- ( ( A \ B ) =/= (/) -> A =/= B )
Theorem	difeq 23951	Rewriting an equation with set difference, without using quantifiers. (Contributed by Thierry Arnoux, 24-Sep-2017.)
|- ( ( A \ B ) = C <-> ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) )
19.3.3.4  Unordered pairs
Theorem	elpreq 23952	Equality wihin a pair (Contributed by Thierry Arnoux, 23-Aug-2017.)
|- ( ph -> X e. { A , B } )   &    |- ( ph -> Y e. { A , B } )   &    |- ( ph -> ( X = A <-> Y = A ) )   =>    |- ( ph -> X = Y )
Theorem	preqsnd 23953	Equivalence for a pair equal to a singleton, deduction form. (Contributed by Thierry Arnoux, 27-Dec-2016.)
|- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> C e. _V )   =>    |- ( ph -> ( { A , B } = { C } <-> ( A = C /\ B = C ) ) )
19.3.3.5  Conditional operator - misc additions
Theorem	ifeqeqx 23954*	An equality theorem tailored for ballotlemsf1o 24724 (Contributed by Thierry Arnoux, 14-Apr-2017.)
|- ( x = X -> A = C )   &    |- ( x = Y -> B = a )   &    |- ( x = X -> ( ch <-> th ) )   &    |- ( x = Y -> ( ch <-> ps ) )   &    |- ( ph -> a = C )   &    |- ( ( ph /\ ps ) -> th )   &    |- ( ph -> Y e. V )   &    |- ( ph -> X e. W )   =>    |- ( ( ph /\ x = if ( ps , X , Y ) ) -> a = if ( ch , A , B ) )
Theorem	ifbieq12d2 23955	Equivalence deduction for conditional operators. (Contributed by Thierry Arnoux, 14-Feb-2017.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ( ph /\ ps ) -> A = C )   &    |- ( ( ph /\ -. ps ) -> B = D )   =>    |- ( ph -> if ( ps , A , B ) = if ( ch , C , D ) )
Theorem	ovif 23956	Move a conditional outside of an operation (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( if ( ph , A , B ) F C ) = if ( ph , ( A F C ) , ( B F C ) )
Theorem	elimifd 23957	Elimination of a conditional operator contained in a wff ch. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( ph -> ( if ( ps , A , B ) = A -> ( ch <-> th ) ) )   &    |- ( ph -> ( if ( ps , A , B ) = B -> ( ch <-> ta ) ) )   =>    |- ( ph -> ( ch <-> ( ( ps /\ th ) \/ ( -. ps /\ ta ) ) ) )
Theorem	elim2if 23958	Elimination of two conditional operators contained in a wff ch. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( if ( ph , A , if ( ps , B , C ) ) = A -> ( ch <-> th ) )   &    |- ( if ( ph , A , if ( ps , B , C ) ) = B -> ( ch <-> ta ) )   &    |- ( if ( ph , A , if ( ps , B , C ) ) = C -> ( ch <-> et ) )   =>    |- ( ch <-> ( ( ph /\ th ) \/ ( -. ph /\ ( ( ps /\ ta ) \/ ( -. ps /\ et ) ) ) ) )
Theorem	elim2ifim 23959	Elimination of two conditional operators for an implication. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( if ( ph , A , if ( ps , B , C ) ) = A -> ( ch <-> th ) )   &    |- ( if ( ph , A , if ( ps , B , C ) ) = B -> ( ch <-> ta ) )   &    |- ( if ( ph , A , if ( ps , B , C ) ) = C -> ( ch <-> et ) )   &    |- ( ph -> th )   &    |- ( ( -. ph /\ ps ) -> ta )   &    |- ( ( -. ph /\ -. ps ) -> et )   =>    |- ch
19.3.3.6  Indexed union - misc additions
Theorem	iuneq12daf 23960	Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 13-Mar-2017.)
|- F/ x ph   &    |- F/_ x A   &    |- F/_ x B   &    |- ( ph -> A = B )   &    |- ( ( ph /\ x e. A ) -> C = D )   =>    |- ( ph -> U_ x e. A C = U_ x e. B D )
Theorem	iuneq12df 23961	Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 31-Dec-2016.)
|- F/ x ph   &    |- F/_ x A   &    |- F/_ x B   &    |- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> U_ x e. A C = U_ x e. B D )
Theorem	ssiun3 23962*	Subset equivalence for an indexed union. (Contributed by Thierry Arnoux, 17-Oct-2016.)
|- ( A. y e. C E. x e. A y e. B <-> C C_ U_ x e. A B )
Theorem	ssiun2sf 23963	Subset relationship for an indexed union. (Contributed by Thierry Arnoux, 31-Dec-2016.)
|- F/_ x A   &    |- F/_ x C   &    |- F/_ x D   &    |- ( x = C -> B = D )   =>    |- ( C e. A -> D C_ U_ x e. A B )
Theorem	iuninc 23964*	The union of an increasing collection of sets is its last element. (Contributed by Thierry Arnoux, 22-Jan-2017.)
|- ( ph -> F Fn NN )   &    |- ( ( ph /\ n e. NN ) -> ( F ` n ) C_ ( F ` ( n + 1 ) ) )   =>    |- ( ( ph /\ i e. NN ) -> U_ n e. ( 1 ... i ) ( F ` n ) = ( F ` i ) )
Theorem	iundifdifd 23965*	The intersection of a set is the complement of the union of the complements. (Contributed by Thierry Arnoux, 19-Dec-2016.)
|- ( A C_ ~P O -> ( A =/= (/) -> |^| A = ( O \ U_ x e. A ( O \ x ) ) ) )
Theorem	iundifdif 23966*	The intersection of a set is the complement of the union of the complements. TODO shorten using iundifdifd 23965 (Contributed by Thierry Arnoux, 4-Sep-2016.)
|- O e. _V   &    |- A C_ ~P O   =>    |- ( A =/= (/) -> |^| A = ( O \ U_ x e. A ( O \ x ) ) )
Theorem	iunrdx 23967*	Re-index an indexed union. (Contributed by Thierry Arnoux, 6-Apr-2017.)
|- ( ph -> F : A -onto-> C )   &    |- ( ( ph /\ y = ( F ` x ) ) -> D = B )   =>    |- ( ph -> U_ x e. A B = U_ y e. C D )
19.3.3.7  Disjointness - misc additions
Theorem	cbvdisjf 23968*	Change bound variables in a disjoint collection. (Contributed by Thierry Arnoux, 6-Apr-2017.)
|- F/_ x A   &    |- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- (Disj x e. A B <-> Disj y e. A C )
Theorem	disjss1f 23969	A subset of a disjoint collection is disjoint. (Contributed by Thierry Arnoux, 6-Apr-2017.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A C_ B -> (Disj x e. B C -> Disj x e. A C ) )
Theorem	disjdifprg 23970*	A trivial partition into a subset and its complement. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( ( A e. V /\ B e. W ) -> Disj x e. { ( B \ A ) , A } x )
Theorem	disjdifprg2 23971*	A trivial partition of a set into its difference and intersection with another set. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( A e. V -> Disj x e. { ( A \ B ) , ( A i^i B ) } x )
Theorem	disji2f 23972*	Property of a disjoint collection: if B ( x ) = C and B ( Y ) = D, and x =/= Y, then B and C are disjoint. (Contributed by Thierry Arnoux, 30-Dec-2016.)
|- F/_ x C   &    |- ( x = Y -> B = C )   =>    |- ( (Disj x e. A B /\ ( x e. A /\ Y e. A ) /\ x =/= Y ) -> ( B i^i C ) = (/) )
Theorem	disjif 23973*	Property of a disjoint collection: if B ( x ) and B ( Y ) = D have a common element Z, then x = Y. (Contributed by Thierry Arnoux, 30-Dec-2016.)
|- F/_ x C   &    |- ( x = Y -> B = C )   =>    |- ( (Disj x e. A B /\ ( x e. A /\ Y e. A ) /\ ( Z e. B /\ Z e. C ) ) -> x = Y )
Theorem	disjorf 23974*	Two ways to say that a collection B ( i ) for i e. A is disjoint. (Contributed by Thierry Arnoux, 8-Mar-2017.)
|- F/_ i A   &    |- F/_ j A   &    |- ( i = j -> B = C )   =>    |- (Disj i e. A B <-> A. i e. A A. j e. A ( i = j \/ ( B i^i C ) = (/) ) )
Theorem	disjorsf 23975*	Two ways to say that a collection B ( i ) for i e. A is disjoint. (Contributed by Thierry Arnoux, 8-Mar-2017.)
|- F/_ x A   =>    |- (Disj x e. A B <-> A. i e. A A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
Theorem	disjif2 23976*	Property of a disjoint collection: if B ( x ) and B ( Y ) = D have a common element Z, then x = Y. (Contributed by Thierry Arnoux, 6-Apr-2017.)
|- F/_ x A   &    |- F/_ x C   &    |- ( x = Y -> B = C )   =>    |- ( (Disj x e. A B /\ ( x e. A /\ Y e. A ) /\ ( Z e. B /\ Z e. C ) ) -> x = Y )
Theorem	disjabrex 23977*	Rewriting a disjoint collection into a partition of its image set (Contributed by Thierry Arnoux, 30-Dec-2016.)
|- (Disj x e. A B -> Disj y e. { z | E. x e. A z = B } y )
Theorem	disjabrexf 23978*	Rewriting a disjoint collection into a partition of its image set (Contributed by Thierry Arnoux, 30-Dec-2016.) (Revised by Thierry Arnoux, 9-Mar-2017.)
|- F/_ x A   =>    |- (Disj x e. A B -> Disj y e. { z | E. x e. A z = B } y )
Theorem	disjpreima 23979*	A preimage of a disjoint set is disjoint. (Contributed by Thierry Arnoux, 7-Feb-2017.)
|- ( ( Fun F /\ Disj x e. A B ) -> Disj x e. A ( `' F " B ) )
Theorem	disjin 23980	If a collection is disjoint, so is the collection of the intersections with a given set. (Contributed by Thierry Arnoux, 14-Feb-2017.)
|- (Disj x e. B C -> Disj x e. B ( C i^i A ) )
Theorem	disjxpin 23981*	Derive a disjunction over a cross product from the disjunctions over its first and second elements. (Contributed by Thierry Arnoux, 9-Mar-2018.)
|- ( x = ( 1st ` p ) -> C = E )   &    |- ( y = ( 2nd ` p ) -> D = F )   &    |- ( ph -> Disj x e. A C )   &    |- ( ph -> Disj y e. B D )   =>    |- ( ph -> Disj p e. ( A X. B ) ( E i^i F ) )
Theorem	iundisjf 23982*	Rewrite a countable union as a disjoint union. Cf. iundisj 19395 (Contributed by Thierry Arnoux, 31-Dec-2016.)
|- F/_ k A   &    |- F/_ n B   &    |- ( n = k -> A = B )   =>    |- U_ n e. NN A = U_ n e. NN ( A \ U_ k e. ( 1..^ n ) B )
Theorem	iundisj2f 23983*	A disjoint union is disjoint. Cf. iundisj2 19396 (Contributed by Thierry Arnoux, 30-Dec-2016.)
|- F/_ k A   &    |- F/_ n B   &    |- ( n = k -> A = B )   =>    |- Disj n e. NN ( A \ U_ k e. ( 1..^ n ) B )
Theorem	disjrdx 23984*	Re-index a disjunct collection statement. (Contributed by Thierry Arnoux, 7-Apr-2017.)
|- ( ph -> F : A -1-1-onto-> C )   &    |- ( ( ph /\ y = ( F ` x ) ) -> D = B )   =>    |- ( ph -> (Disj x e. A B <-> Disj y e. C D ) )
Theorem	disjex 23985*	Two ways to say that two classes are disjoint (or equal). (Contributed by Thierry Arnoux, 4-Oct-2016.)
|- ( ( E. z ( z e. A /\ z e. B ) -> A = B ) <-> ( A = B \/ ( A i^i B ) = (/) ) )
Theorem	disjexc 23986*	A variant of disjex 23985, applicable for more generic families. (Contributed by Thierry Arnoux, 4-Oct-2016.)
|- ( x = y -> A = B )   =>    |- ( ( E. z ( z e. A /\ z e. B ) -> x = y ) -> ( A = B \/ ( A i^i B ) = (/) ) )
19.3.4  Relations and Functions
19.3.4.1  Relations - misc additions
Theorem	dfrel4 23987*	A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 5731 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.) (Revised by Thierry Arnoux, 11-May-2017.)
|- F/_ x R   &    |- F/_ y R   =>    |- ( Rel R <-> R = { <. x , y >. | x R y } )
Theorem	rnpropg 23988	The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.)
|- ( ( A e. V /\ B e. W ) -> ran { <. A , C >. , <. B , D >. } = { C , D } )
Theorem	xpdisjres 23989	Restriction of a constant function (or other cross product) outside of its domain (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( ( A i^i C ) = (/) -> ( ( A X. B ) |` C ) = (/) )
Theorem	csbcnvg 23990	Move class substitution in and out of the converse of a function. (Contributed by Thierry Arnoux, 8-Feb-2017.)
|- ( A e. V -> `' [_ A / x ]_ F = [_ A / x ]_ `' F )
Theorem	imadifxp 23991	Image of the difference with a cross product (Contributed by Thierry Arnoux, 13-Dec-2017.)
|- ( C C_ A -> ( ( R \ ( A X. B ) ) " C ) = ( ( R " C ) \ B ) )
19.3.4.2  Functions - misc additions
Theorem	fdmrn 23992	A different way to write F is a function. (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- ( Fun F <-> F : dom F --> ran F )
Theorem	nvof1o 23993	An involution is a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- ( ( F Fn A /\ `' F = F ) -> F : A -1-1-onto-> A )
Theorem	f1o3d 23994*	Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017.)
|- ( ph -> F = ( x e. A |-> C ) )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( ( ph /\ y e. B ) -> D e. A )   &    |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x = D <-> y = C ) )   =>    |- ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( y e. B |-> D ) ) )
Theorem	rinvf1o 23995	Sufficient conditions for the restriction of an involution to be a bijection (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- Fun F   &    |- `' F = F   &    |- ( F " A ) C_ B   &    |- ( F " B ) C_ A   &    |- A C_ dom F   &    |- B C_ dom F   =>    |- ( F |` A ) : A -1-1-onto-> B
Theorem	dfimafnf 23996*	Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Thierry Arnoux, 24-Apr-2017.)
|- F/_ x A   &    |- F/_ x F   =>    |- ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = { y | E. x e. A y = ( F ` x ) } )
Theorem	funimass4f 23997	Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017.)
|- F/_ x A   &    |- F/_ x B   &    |- F/_ x F   =>    |- ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )
Theorem	mptcnv 23998*	The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017.)
|- ( ph -> ( ( x e. A /\ y = B ) <-> ( y e. C /\ x = D ) ) )   =>    |- ( ph -> `' ( x e. A |-> B ) = ( y e. C |-> D ) )
Theorem	fneq12 23999	Equality theorem for function predicate with domain. (Contributed by Thierry Arnoux, 31-Jan-2017.)
|- ( ( F = G /\ A = B ) -> ( F Fn A <-> G Fn B ) )
Theorem	fimacnvinrn 24000	Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 21-Jan-2017.)
|- ( Fun F -> ( `' F " A ) = ( `' F " ( A i^i ran F ) ) )