P. 294 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29301-29400   *Has distinct variable group(s)

Type	Label	Description
Statement
PART 20  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)
20.1  Mathboxes for user contributions
20.1.1  Mathbox guidelines
Theorem	mathbox 29301	(This theorem is a dummy placeholder for these guidelines. The label of this theorem, "mathbox", is hard-coded into the metamath program to identify the start of the mathbox section for web page generation.) A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm. For contributors: By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm. Mathboxes are provided to help keep your work synchronized with changes in set.mm while allowing you to work independently without affecting other contributors. Even though in a sense your mathbox belongs to you, it is still part of the shared body of knowledge contained in set.mm, and occasionally other people may make maintenance edits to your mathbox for things like keeping it synchronized with the rest of set.mm, reducing proof lengths, moving your theorems to the main part of set.mm when needed, and fixing typos or other errors. If you want to preserve it the way you left it, you can keep a local copy or keep track of the GitHub commit number. Guidelines: 1. See conventions 27258 for our general style guidelines. For contributing via GitHub, see https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md. The metamath program command "verify markup *" will check that you have followed many of of the conventions we use. 2. If at all possible, please use only nullary class constants for new definitions, for example as in df-div 10685. 3. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The metamath program command "write source set.mm /rewrap" will take care of our indentation conventions and line wrapping. 4. All mathbox content will be on public display and should hopefully reflect the overall quality of the website. 5. Mathboxes must be independent from one another (checked by "verify markup *"). If you need a theorem from another mathbox, typically it is moved to the main part of set.mm. New users should consult with more experienced users before doing this. (Contributed by NM, 20-Feb-2007.) (New usage is discouraged.)
|- ph   =>    |- ph
20.2  Mathbox for Stefan Allan
Theorem	foo3 29302	A theorem about the universal class. (Contributed by Stefan Allan, 9-Dec-2008.)
|- ph   =>    |- _V = { x | ph }
Theorem	xfree 29303	A partial converse to 19.9t 2071. (Contributed by Stefan Allan, 21-Dec-2008.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- ( A. x ( ph -> A. x ph ) <-> A. x ( E. x ph -> ph ) )
Theorem	xfree2 29304	A partial converse to 19.9t 2071. (Contributed by Stefan Allan, 21-Dec-2008.)
|- ( A. x ( ph -> A. x ph ) <-> A. x ( -. ph -> A. x -. ph ) )
Theorem	addltmulALT 29305	A proof readability experiment for addltmul 11268. (Contributed by Stefan Allan, 30-Oct-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 2 < A /\ 2 < B ) ) -> ( A + B ) < ( A x. B ) )
20.3  Mathbox for Thierry Arnoux
20.3.1  Propositional Calculus - misc additions
Theorem	bian1d 29306	Adding a superfluous conjunct in a biconditional. (Contributed by Thierry Arnoux, 26-Feb-2017.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ph -> ( ( ch /\ ps ) <-> ( ch /\ th ) ) )
Theorem	or3di 29307	Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.)
|- ( ( ph \/ ( ps /\ ch /\ ta ) ) <-> ( ( ph \/ ps ) /\ ( ph \/ ch ) /\ ( ph \/ ta ) ) )
Theorem	or3dir 29308	Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.)
|- ( ( ( ph /\ ps /\ ch ) \/ ta ) <-> ( ( ph \/ ta ) /\ ( ps \/ ta ) /\ ( ch \/ ta ) ) )
Theorem	3o1cs 29309	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
|- ( ( ph \/ ps \/ ch ) -> th )   =>    |- ( ph -> th )
Theorem	3o2cs 29310	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
|- ( ( ph \/ ps \/ ch ) -> th )   =>    |- ( ps -> th )
Theorem	3o3cs 29311	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
|- ( ( ph \/ ps \/ ch ) -> th )   =>    |- ( ch -> th )
20.3.2  Predicate Calculus
20.3.2.1  Predicate Calculus - misc additions
Theorem	spc2ed 29312*	Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017.)
|- F/ x ch   &    |- F/ y ch   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )   =>    |- ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( ch -> E. x E. y ps ) )
Theorem	spc2d 29313*	Specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017.)
|- F/ x ch   &    |- F/ y ch   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )   =>    |- ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( A. x A. y ps -> ch ) )
Theorem	vtocl2d 29314*	Implicit substitution of two classes for two setvar variables. (Contributed by Thierry Arnoux, 25-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ( x = A /\ y = B ) -> ( ps <-> ch ) )   &    |- ( ph -> ps )   =>    |- ( ph -> ch )
Theorem	eqri 29315	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
20.3.2.2  Restricted quantification - misc additions
Theorem	ralcom4f 29316*	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 29317*	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	19.9d2rf 29318	A deduction version of one direction of 19.9 2072 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 29319*	A deduction version of one direction of 19.9 2072 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.29ffa 29320*	A commonly used pattern based on r19.29 3072, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)
|- ( ( ( ( ph /\ x e. A ) /\ y e. B ) /\ ps ) -> ch )   =>    |- ( ( ph /\ E. x e. A E. y e. B ps ) -> ch )
20.3.2.3  Substitution (without distinct variables) - misc additions
Theorem	sbceqbidf 29321	Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018.)
|- F/ x ph   &    |- ( ph -> A = B )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( [. A / x ]. ps <-> [. B / x ]. ch ) )
Theorem	sbcies 29322*	A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 14-Mar-2019.)
|- A = ( E ` W )   &    |- ( a = A -> ( ph <-> ps ) )   =>    |- ( w = W -> ( [. ( E ` w ) / a ]. ps <-> ph ) )
20.3.2.4  Existential "at most one" - misc additions
Theorem	moel 29323*	"At most one" element in a set. (Contributed by Thierry Arnoux, 26-Jul-2018.)
|- ( E* x x e. A <-> A. x e. A A. y e. A x = y )
Theorem	mo5f 29324*	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 29325*	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 29326*	"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 ) )
Theorem	rmoeqALT 29327*	Equality's restricted existential "at most one" property. (Contributed by Thierry Arnoux, 30-Mar-2018.) Obsolete version of rmoeq 3405 as of 27-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. V -> E* x e. B x = A )
20.3.2.5  Existential uniqueness - misc additions
Theorem	2reuswap2 29328*	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 29329*	Transfer existential uniqueness from a variable x to another variable y contained in expression A. Cf. reuxfr2d 4891. (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 29330*	Transfer existential uniqueness from a variable x to another variable y contained in expression A. Cf. reuxfrd 4893. (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 29331*	Restricted existential quantification over the union of the range of a function. Cf. rexrn 6361 and eluni2 4440. (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 )
20.3.2.6  Restricted "at most one" - misc additions
Theorem	rmoxfrdOLD 29332*	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 29333*	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 29334	"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 29335*	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 29336*	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 29337*	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 ) )
20.3.3  General Set Theory
20.3.3.1  Class abstractions (a.k.a. class builders)
Theorem	rabrab 29338	Abstract builder restricted to another restricted abstract builder. (Contributed by Thierry Arnoux, 30-Aug-2017.)
|- { x e. { x e. A | ph } | ps } = { x e. A | ( ph /\ ps ) }
Theorem	difrab2 29339	Difference of two restricted class abstractions. Compare with difrab 3901. (Contributed by Thierry Arnoux, 3-Jan-2022.)
|- ( { x e. A | ph } \ { x e. B | ph } ) = { x e. ( A \ B ) | ph }
Theorem	rabexgfGS 29340	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 )
Theorem	rabsnel 29341*	Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by Thierry Arnoux, 15-Sep-2018.)
|- B e. _V   =>    |- ( { x e. A | ph } = { B } -> B e. A )
Theorem	rabeqsnd 29342*	Conditions for a restricted class abstraction to be a singleton, in deduction form. (Contributed by Thierry Arnoux, 2-Dec-2021.)
|- ( x = B -> ( ps <-> ch ) )   &    |- ( ph -> B e. A )   &    |- ( ph -> ch )   &    |- ( ( ( ph /\ x e. A ) /\ ps ) -> x = B )   =>    |- ( ph -> { x e. A | ps } = { B } )
Theorem	foresf1o 29343*	From a surjective function, *choose* a subset of the domain, such that the restricted function is bijective. (Contributed by Thierry Arnoux, 27-Jan-2020.)
|- ( ( A e. V /\ F : A -onto-> B ) -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> B )
Theorem	rabfodom 29344*	Domination relation for restricted abstract class builders, based on a surjective function. (Contributed by Thierry Arnoux, 27-Jan-2020.)
|- ( ( ph /\ x e. A /\ y = ( F ` x ) ) -> ( ch <-> ps ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A -onto-> B )   =>    |- ( ph -> { y e. B | ch } ~<_ { x e. A | ps } )
20.3.3.2  Image Sets
Theorem	abrexdomjm 29345*	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 29346*	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 29347*	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 29348*	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 29349*	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 29350*	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 )
20.3.3.3  Set relations and operations - misc additions
Theorem	rabss3d 29351*	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 29352	Intersection with an intersection. (Contributed by Thierry Arnoux, 27-Dec-2016.)
|- ( A i^i ( A i^i B ) ) = ( A i^i B )
Theorem	inindif 29353	See inundif 4046. (Contributed by Thierry Arnoux, 13-Sep-2017.)
|- ( ( A i^i C ) i^i ( A \ C ) ) = (/)
Theorem	difininv 29354	Condition for the intersections of two sets with a given set to be equal. (Contributed by Thierry Arnoux, 28-Dec-2021.)
|- ( ( ( ( A \ C ) i^i B ) = (/) /\ ( ( C \ A ) i^i B ) = (/) ) -> ( A i^i B ) = ( C i^i B ) )
Theorem	difeq 29355	Rewriting an equation with class difference, without using quantifiers. (Contributed by Thierry Arnoux, 24-Sep-2017.)
|- ( ( A \ B ) = C <-> ( ( C i^i B ) = (/) /\ ( C u. B ) = ( A u. B ) ) )
Theorem	indifundif 29356	A remarkable equation with sets. (Contributed by Thierry Arnoux, 18-May-2020.)
|- ( ( ( A i^i B ) \ C ) u. ( A \ B ) ) = ( A \ ( B i^i C ) )
Theorem	elpwincl1 29357	Closure of intersection with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.)
|- ( ph -> A e. ~P C )   =>    |- ( ph -> ( A i^i B ) e. ~P C )
Theorem	elpwdifcl 29358	Closure of class difference with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.)
|- ( ph -> A e. ~P C )   =>    |- ( ph -> ( A \ B ) e. ~P C )
Theorem	elpwiuncl 29359*	Closure of indexed union with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 27-May-2020.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ~P C )   =>    |- ( ph -> U_ k e. A B e. ~P C )
20.3.3.4  Unordered pairs
Theorem	elpreq 29360	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 )
20.3.3.5  Conditional operator - misc additions
Theorem	ifeqeqx 29361*	An equality theorem tailored for ballotlemsf1o 30575. (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	elimifd 29362	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 29363	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 29364	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
Theorem	ifeq3da 29365	Given an expression C containing if ( ps , E , F ), substitute (hypotheses .1 and .2) and evaluate (hypotheses .3 and .4) it for both cases at the same time. (Contributed by Thierry Arnoux, 13-Dec-2021.)
|- ( if ( ps , E , F ) = E -> C = G )   &    |- ( if ( ps , E , F ) = F -> C = H )   &    |- ( ph -> G = A )   &    |- ( ph -> H = B )   =>    |- ( ph -> if ( ps , A , B ) = C )
20.3.3.6  Set union
Theorem	uniinn0 29366*	Sufficient and necessary condition for a union to intersect with a given set. (Contributed by Thierry Arnoux, 27-Jan-2020.)
|- ( ( U. A i^i B ) =/= (/) <-> E. x e. A ( x i^i B ) =/= (/) )
Theorem	uniin1 29367*	Union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. (Contributed by Thierry Arnoux, 21-Jun-2020.)
|- U_ x e. A ( x i^i B ) = ( U. A i^i B )
Theorem	uniin2 29368*	Union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. (Contributed by Thierry Arnoux, 21-Jun-2020.)
|- U_ x e. B ( A i^i x ) = ( A i^i U. B )
Theorem	difuncomp 29369	Express a class difference using unions and class complements. (Contributed by Thierry Arnoux, 21-Jun-2020.)
|- ( A C_ C -> ( A \ B ) = ( C \ ( ( C \ A ) u. B ) ) )
Theorem	pwuniss 29370	Condition for a class union to be a subset. (Contributed by Thierry Arnoux, 21-Jun-2020.)
|- ( A C_ ~P B -> U. A C_ B )
Theorem	elpwunicl 29371	Closure of a set union with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 21-Jun-2020.)
|- ( ph -> B e. V )   &    |- ( ph -> A e. ~P ~P B )   =>    |- ( ph -> U. A e. ~P B )
20.3.3.7  Indexed union - misc additions
Theorem	cbviunf 29372*	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.)
|- F/_ x A   &    |- F/_ y A   &    |- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- U_ x e. A B = U_ y e. A C
Theorem	iuneq12daf 29373	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	iunin1f 29374	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4573 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.) (Revised by Thierry Arnoux, 2-May-2020.)
|- F/_ x C   =>    |- U_ x e. A ( B i^i C ) = ( U_ x e. A B i^i C )
Theorem	iunxsngf 29375*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.) (Revised by Thierry Arnoux, 2-May-2020.)
|- F/_ x C   &    |- ( x = A -> B = C )   =>    |- ( A e. V -> U_ x e. { A } B = C )
Theorem	ssiun3 29376*	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	iinssiun 29377*	An indexed intersection is a subset of the corresponding indexed union. (Contributed by Thierry Arnoux, 31-Dec-2021.)
|- ( A =/= (/) -> |^|_ x e. A B C_ U_ x e. A B )
Theorem	ssiun2sf 29378	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 29379*	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 29380*	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 29381*	The intersection of a set is the complement of the union of the complements. TODO: shorten using iundifdifd 29380. (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 29382*	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 )
Theorem	iunpreima 29383*	Preimage of an indexed union. (Contributed by Thierry Arnoux, 27-Mar-2018.)
|- ( Fun F -> ( `' F " U_ x e. A B ) = U_ x e. A ( `' F " B ) )
20.3.3.8  Disjointness - misc additions
Theorem	disjnf 29384*	In case x is not free in B, disjointness is not so interesting since it reduces to cases where A is a singleton. (Google Groups discussion with Peter Mazsa.) (Contributed by Thierry Arnoux, 26-Jul-2018.)
|- (Disj x e. A B <-> ( B = (/) \/ E* x x e. A ) )
Theorem	cbvdisjf 29385*	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 29386	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	disjeq1f 29387	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A = B -> (Disj x e. A C <-> Disj x e. B C ) )
Theorem	disjdifprg 29388*	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 29389*	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 29390*	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 29391*	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 29392*	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 29393*	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 29394*	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 29395*	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 29396*	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 29397*	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	disjrnmpt 29398*	Rewriting a disjoint collection using the range of a mapping. (Contributed by Thierry Arnoux, 27-May-2020.)
|- (Disj x e. A B -> Disj y e. ran ( x e. A |-> B ) y )
Theorem	disjin 29399	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	disjin2 29400	If a collection is disjoint, so is the collection of the intersections with a given set. (Contributed by Thierry Arnoux, 21-Jun-2020.)
|- (Disj x e. B C -> Disj x e. B ( A i^i C ) )