P. 359 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35801-35900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ifpim1 35801	Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph -> ps ) <-> if- ( -. ph , T. , ps ) )
Theorem	ifpnot 35802	Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( -. ph <-> if- ( ph , F. , T. ) )
Theorem	ifpid2 35803	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ph <-> if- ( ph , T. , F. ) )
Theorem	ifpim2 35804	Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph -> ps ) <-> if- ( ps , T. , -. ph ) )
Theorem	ifpbi23 35805	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> (if- ( ta , ph , ch ) <-> if- ( ta , ps , th ) ) )
Theorem	ifpdfbi 35806	Define biimplication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph <-> ps ) <-> if- ( ph , ps , -. ps ) )
Theorem	ifpbiidcor 35807	Restatement of biid 239. (Contributed by RP, 25-Apr-2020.)
|- if- ( ph , ph , -. ph )
Theorem	ifpbicor 35808	Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , ps , -. ps ) <-> if- ( ps , ph , -. ph ) )
Theorem	ifpxorcor 35809	Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , -. ps , ps ) <-> if- ( ps , -. ph , ph ) )
Theorem	ifpbi1 35810	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
|- ( ( ph <-> ps ) -> (if- ( ph , ch , th ) <-> if- ( ps , ch , th ) ) )
Theorem	ifpnot23 35811	Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.)
|- ( -. if- ( ph , ps , ch ) <-> if- ( ph , -. ps , -. ch ) )
Theorem	ifpnotnotb 35812	Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , -. ps , -. ch ) <-> -. if- ( ph , ps , ch ) )
Theorem	ifpnorcor 35813	Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , -. ph , -. ps ) <-> if- ( ps , -. ps , -. ph ) )
Theorem	ifpnancor 35814	Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , -. ps , -. ph ) <-> if- ( ps , -. ph , -. ps ) )
Theorem	ifpnot23b 35815	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
|- ( -. if- ( ph , -. ps , ch ) <-> if- ( ph , ps , -. ch ) )
Theorem	ifpbiidcor2 35816	Restatement of biid 239. (Contributed by RP, 25-Apr-2020.)
|- -. if- ( ph , -. ph , ph )
Theorem	ifpnot23c 35817	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
|- ( -. if- ( ph , ps , -. ch ) <-> if- ( ph , -. ps , ch ) )
Theorem	ifpnot23d 35818	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
|- ( -. if- ( ph , -. ps , -. ch ) <-> if- ( ph , ps , ch ) )
Theorem	ifpdfnan 35819	Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph -/\ ps ) <-> if- ( ph , -. ps , T. ) )
Theorem	ifpdfxor 35820	Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph \/_ ps ) <-> if- ( ph , -. ps , ps ) )
Theorem	ifpbi12 35821	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> (if- ( ph , ch , ta ) <-> if- ( ps , th , ta ) ) )
Theorem	ifpbi13 35822	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> (if- ( ph , ta , ch ) <-> if- ( ps , ta , th ) ) )
Theorem	ifpbi123 35823	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> (if- ( ph , ch , ta ) <-> if- ( ps , th , et ) ) )
Theorem	ifpidg 35824	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( th <-> if- ( ph , ps , ch ) ) <-> ( ( ( ( ph /\ ps ) -> th ) /\ ( ( ph /\ th ) -> ps ) ) /\ ( ( ch -> ( ph \/ th ) ) /\ ( th -> ( ph \/ ch ) ) ) ) )
Theorem	ifpid3g 35825	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ch <-> if- ( ph , ps , ch ) ) <-> ( ( ( ph /\ ps ) -> ch ) /\ ( ( ph /\ ch ) -> ps ) ) )
Theorem	ifpid2g 35826	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ps <-> if- ( ph , ps , ch ) ) <-> ( ( ps -> ( ph \/ ch ) ) /\ ( ch -> ( ph \/ ps ) ) ) )
Theorem	ifpid1g 35827	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph <-> if- ( ph , ps , ch ) ) <-> ( ( ch -> ph ) /\ ( ph -> ps ) ) )
Theorem	ifpim23g 35828	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
|- ( ( ( ph -> ps ) <-> if- ( ch , ps , -. ph ) ) <-> ( ( ( ph /\ ps ) -> ch ) /\ ( ch -> ( ph \/ ps ) ) ) )
Theorem	ifpim3 35829	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
|- ( ( ph -> ps ) <-> if- ( ph , ps , -. ph ) )
Theorem	ifpnim1 35830	Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
|- ( -. ( ph -> ps ) <-> if- ( ph , -. ps , ph ) )
Theorem	ifpim4 35831	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
|- ( ( ph -> ps ) <-> if- ( ps , ps , -. ph ) )
Theorem	ifpnim2 35832	Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
|- ( -. ( ph -> ps ) <-> if- ( ps , -. ps , ph ) )
Theorem	ifpim123g 35833	Implication of conditional logical operators. The right hand side is basically conjunctive normal form which is useful in proofs. (Contributed by RP, 16-Apr-2020.)
|- ( (if- ( ph , ch , ta ) -> if- ( ps , th , et ) ) <-> ( ( ( ( ph -> -. ps ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( ta -> th ) ) ) /\ ( ( ( ph -> ps ) \/ ( ch -> et ) ) /\ ( ( -. ps -> ph ) \/ ( ta -> et ) ) ) ) )
Theorem	ifpim1g 35834	Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
|- ( (if- ( ph , ch , th ) -> if- ( ps , ch , th ) ) <-> ( ( ( ps -> ph ) \/ ( th -> ch ) ) /\ ( ( ph -> ps ) \/ ( ch -> th ) ) ) )
Theorem	ifp1bi 35835	Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020.)
|- ( (if- ( ph , ch , th ) <-> if- ( ps , ch , th ) ) <-> ( ( ( ( ph -> ps ) \/ ( ch -> th ) ) /\ ( ( ph -> ps ) \/ ( th -> ch ) ) ) /\ ( ( ( ps -> ph ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( th -> ch ) ) ) ) )
Theorem	ifpbi1b 35836	When the first variable is irrelevant, it can be replaced. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , ch , ch ) <-> if- ( ps , ch , ch ) )
Theorem	ifpimimb 35837	Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , ( ps -> ch ) , ( th -> ta ) ) <-> (if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) )
Theorem	ifpororb 35838	Factor conditional logic operator over disjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , ( ps \/ ch ) , ( th \/ ta ) ) <-> (if- ( ph , ps , th ) \/ if- ( ph , ch , ta ) ) )
Theorem	ifpananb 35839	Factor conditional logic operator over conjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , ( ps /\ ch ) , ( th /\ ta ) ) <-> (if- ( ph , ps , th ) /\ if- ( ph , ch , ta ) ) )
Theorem	ifpnannanb 35840	Factor conditional logic operator over nand in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , ( ps -/\ ch ) , ( th -/\ ta ) ) <-> (if- ( ph , ps , th ) -/\ if- ( ph , ch , ta ) ) )
Theorem	ifpor123g 35841	Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
|- ( (if- ( ph , ch , ta ) \/ if- ( ps , th , et ) ) <-> ( ( ( ( ph -> -. ps ) \/ ( ch \/ th ) ) /\ ( ( ps -> ph ) \/ ( ta \/ th ) ) ) /\ ( ( ( ph -> ps ) \/ ( ch \/ et ) ) /\ ( ( -. ps -> ph ) \/ ( ta \/ et ) ) ) ) )
Theorem	ifpimim 35842	Consequnce of implication. (Contributed by RP, 17-Apr-2020.)
|- (if- ( ph , ( ps -> ch ) , ( th -> ta ) ) -> (if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) )
Theorem	ifpbibib 35843	Factor conditional logic operator over biimplication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , ( ps <-> ch ) , ( th <-> ta ) ) <-> (if- ( ph , ps , th ) <-> if- ( ph , ch , ta ) ) )
Theorem	ifpxorxorb 35844	Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , ( ps \/_ ch ) , ( th \/_ ta ) ) <-> (if- ( ph , ps , th ) \/_ if- ( ph , ch , ta ) ) )
21.25.1.2  Sophisms
Theorem	rp-fakeimass 35845	A special case where implication appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
|- ( ( ph \/ ch ) <-> ( ( ( ph -> ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) )
Theorem	rp-fakeanorass 35846	A special case where a mixture of and and or appears to conform to a mixed associative law. (Contributed by Richard Penner, 26-Feb-2020.)
|- ( ( ch -> ph ) <-> ( ( ( ph /\ ps ) \/ ch ) <-> ( ph /\ ( ps \/ ch ) ) ) )
Theorem	rp-fakeoranass 35847	A special case where a mixture of or and and appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
|- ( ( ph -> ch ) <-> ( ( ( ph \/ ps ) /\ ch ) <-> ( ph \/ ( ps /\ ch ) ) ) )
Theorem	rp-fakenanass 35848	A special case where nand appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
|- ( ( ph <-> ch ) <-> ( ( ( ph -/\ ps ) -/\ ch ) <-> ( ph -/\ ( ps -/\ ch ) ) ) )
Theorem	rp-fakeinunass 35849	A special case where a mixture of intersection and union appears to conform to a mixed associative law. (Contributed by Richard Penner, 26-Feb-2020.)
|- ( C C_ A <-> ( ( A i^i B ) u. C ) = ( A i^i ( B u. C ) ) )
Theorem	rp-fakeuninass 35850	A special case where a mixture of union and intersection appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
|- ( A C_ C <-> ( ( A u. B ) i^i C ) = ( A u. ( B i^i C ) ) )
21.25.1.3  Finite Sets Membership in the class of finite sets can be expressed in many ways.
Theorem	rp-isfinite5 35851*	A set is said to be finite if it can be put in one-to-one correspondence with all the natural numbers between 1 and some n e. NN0. (Contributed by Richard Penner, 3-Mar-2020.)
|- ( A e. Fin <-> E. n e. NN0 ( 1 ... n ) ~~ A )
Theorem	rp-isfinite6 35852*	A set is said to be finite if it is either empty or it can be put in one-to-one correspondence with all the natural numbers between 1 and some n e. NN. (Contributed by Richard Penner, 10-Mar-2020.)
|- ( A e. Fin <-> ( A = (/) \/ E. n e. NN ( 1 ... n ) ~~ A ) )
21.25.1.4  Infinite Sets
Theorem	pwelg 35853*	The powerclass is an element of a class closed under union and powerclass operations iff the element is a member of that class. (Contributed by RP, 21-Mar-2020.)
|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( A e. B <-> ~P A e. B ) )
Theorem	pwinfig 35854*	The powerclass of an infinite set is an infinite set, and vice-versa. Here B is a class which is closed under both the union and the powerclass operations and which may have infinite sets as members. (Contributed by RP, 21-Mar-2020.)
|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( A e. ( B \ Fin ) <-> ~P A e. ( B \ Fin ) ) )
Theorem	pwinfi2 35855	The powerclass of an infinite set is an infinite set, and vice-versa. Here U is a weak universe. (Contributed by RP, 21-Mar-2020.)
|- ( U e. WUni -> ( A e. ( U \ Fin ) <-> ~P A e. ( U \ Fin ) ) )
Theorem	pwinfi3 35856	The powerclass of an infinite set is an infinite set, and vice-versa. Here T is a transitive Tarski universe. (Contributed by RP, 21-Mar-2020.)
|- ( ( T e. Tarski /\ Tr T ) -> ( A e. ( T \ Fin ) <-> ~P A e. ( T \ Fin ) ) )
Theorem	pwinfi 35857	The powerclass of an infinite set is an infinite set, and vice-versa. (Contributed by RP, 21-Mar-2020.)
|- ( A e. ( _V \ Fin ) <-> ~P A e. ( _V \ Fin ) )
21.25.1.5  Finite intersection property While there is not yet a definition, the finite intersection property of a class is introduced by fiint 7854 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 5473, ordelinel 5540 ), chains of sets ordered by the proper subset relation (sorpssin 6593), various sets in the field of topology (inopn 19851, incld 19980, innei 20063, ... ) and "universal" classes like weak universes (wunin 9137, tskin 9183) and the class of all sets (inex1g 4568) .
Theorem	fipjust 35858*	A definition of the finite intersection property of a class based on closure under pair-wise intersection of its elements is independent of the dummy variables. (Contributed by Richard Penner, 1-Jan-2020.)
|- ( A. u e. A A. v e. A ( u i^i v ) e. A <-> A. x e. A A. y e. A ( x i^i y ) e. A )
Theorem	cllem0 35859*	The class of all sets with property ph ( z ) is closed under the binary operation on sets defined in R ( x , y ). (Contributed by Richard Penner, 3-Jan-2020.)
|- V = { z | ph }   &    |- R e. U   &    |- ( z = R -> ( ph <-> ps ) )   &    |- ( z = x -> ( ph <-> ch ) )   &    |- ( z = y -> ( ph <-> th ) )   &    |- ( ( ch /\ th ) -> ps )   =>    |- A. x e. V A. y e. V R e. V
Theorem	superficl 35860*	The class of all supersets of a class has the finite intersection property. (Contributed by Richard Penner, 1-Jan-2020.) (Proof shortened by Richard Penner, 3-Jan-2020.)
|- A = { z | B C_ z }   =>    |- A. x e. A A. y e. A ( x i^i y ) e. A
Theorem	superuncl 35861*	The class of all supersets of a class is closed under binary union. (Contributed by Richard Penner, 3-Jan-2020.)
|- A = { z | B C_ z }   =>    |- A. x e. A A. y e. A ( x u. y ) e. A
Theorem	ssficl 35862*	The class of all subsets of a class has the finite intersection property. (Contributed by Richard Penner, 1-Jan-2020.) (Proof shortened by Richard Penner, 3-Jan-2020.)
|- A = { z | z C_ B }   =>    |- A. x e. A A. y e. A ( x i^i y ) e. A
Theorem	ssuncl 35863*	The class of all subsets of a class is closed under binary union. (Contributed by Richard Penner, 3-Jan-2020.)
|- A = { z | z C_ B }   =>    |- A. x e. A A. y e. A ( x u. y ) e. A
Theorem	ssdifcl 35864*	The class of all subsets of a class is closed under set difference. (Contributed by Richard Penner, 3-Jan-2020.)
|- A = { z | z C_ B }   =>    |- A. x e. A A. y e. A ( x \ y ) e. A
Theorem	sssymdifcl 35865*	The class of all subsets of a class is closed under symmetric difference. (Contributed by Richard Penner, 3-Jan-2020.)
|- A = { z | z C_ B }   =>    |- A. x e. A A. y e. A ( ( x \ y ) u. ( y \ x ) ) e. A
Theorem	fiinfi 35866*	If two classes have the finite intersection property, then so does their intersection. (Contributed by Richard Penner, 1-Jan-2020.)
|- ( ph -> A. x e. A A. y e. A ( x i^i y ) e. A )   &    |- ( ph -> A. x e. B A. y e. B ( x i^i y ) e. B )   &    |- ( ph -> C = ( A i^i B ) )   =>    |- ( ph -> A. x e. C A. y e. C ( x i^i y ) e. C )
21.25.2  Additional statements on relations and subclasses
Theorem	al3im 35867	Version of ax-4 1678 for a nested implication. (Contributed by RP, 13-Apr-2020.)
|- ( A. x ( ph -> ( ps -> ( ch -> th ) ) ) -> ( A. x ph -> ( A. x ps -> ( A. x ch -> A. x th ) ) ) )
Theorem	intima0 35868*	Two ways of expressing the intersection of images of a class. (Contributed by RP, 13-Apr-2020.)
|- |^|_ a e. A ( a " B ) = |^| { x | E. a e. A x = ( a " B ) }
Theorem	elimaint 35869*	Element of image of intersection. (Contributed by RP, 13-Apr-2020.)
|- ( y e. ( |^| A " B ) <-> E. b e. B A. a e. A <. b , y >. e. a )
Theorem	csbcog 35870	Distribute proper substitution through a composition of relations. (Contributed by RP, 28-Jun-2020.)
|- ( A e. V -> [_ A / x ]_ ( B o. C ) = ( [_ A / x ]_ B o. [_ A / x ]_ C ) )
Theorem	cnviun 35871*	Converse of indexed union. (Contributed by RP, 20-Jun-2020.)
|- `' U_ x e. A B = U_ x e. A `' B
Theorem	imaiun1 35872*	The image of an indexed union is the indexed union of the images. (Contributed by RP, 29-Jun-2020.)
|- ( U_ x e. A B " C ) = U_ x e. A ( B " C )
Theorem	coiun1 35873*	Composition with an indexed union. Proof analgous to that of coiun 5365. (Contributed by RP, 20-Jun-2020.)
|- ( U_ x e. C A o. B ) = U_ x e. C ( A o. B )
Theorem	elintima 35874*	Element of intersection of images. (Contributed by RP, 13-Apr-2020.)
|- ( y e. |^| { x | E. a e. A x = ( a " B ) } <-> A. a e. A E. b e. B <. b , y >. e. a )
Theorem	intimass 35875*	The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.)
|- ( |^| A " B ) C_ |^| { x | E. a e. A x = ( a " B ) }
Theorem	intimass2 35876*	The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.)
|- ( |^| A " B ) C_ |^|_ x e. A ( x " B )
Theorem	intimag 35877*	Requirement for the image under the intersection of relations to equal the intersection of the images of those relations. (Contributed by RP, 13-Apr-2020.)
|- ( A. y ( A. a e. A E. b e. B <. b , y >. e. a -> E. b e. B A. a e. A <. b , y >. e. a ) -> ( |^| A " B ) = |^| { x | E. a e. A x = ( a " B ) } )
Theorem	intimasn 35878*	Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020.)
|- ( B e. V -> ( |^| A " { B } ) = |^| { x | E. a e. A x = ( a " { B } ) } )
Theorem	intimasn2 35879*	Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020.)
|- ( B e. V -> ( |^| A " { B } ) = |^|_ x e. A ( x " { B } ) )
Theorem	ss2iundf 35880*	Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.)
|- F/ x ph   &    |- F/ y ph   &    |- F/_ y Y   &    |- F/_ y A   &    |- F/_ y B   &    |- F/_ x C   &    |- F/_ y C   &    |- F/_ x D   &    |- F/_ y G   &    |- ( ( ph /\ x e. A ) -> Y e. C )   &    |- ( ( ph /\ x e. A /\ y = Y ) -> D = G )   &    |- ( ( ph /\ x e. A ) -> B C_ G )   =>    |- ( ph -> U_ x e. A B C_ U_ y e. C D )
Theorem	ss2iundv 35881*	Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.)
|- ( ( ph /\ x e. A ) -> Y e. C )   &    |- ( ( ph /\ x e. A /\ y = Y ) -> D = G )   &    |- ( ( ph /\ x e. A ) -> B C_ G )   =>    |- ( ph -> U_ x e. A B C_ U_ y e. C D )
Theorem	cbviuneq12df 35882*	Rule used to change the bound variables and classes in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by RP, 17-Jul-2020.)
|- F/ x ph   &    |- F/ y ph   &    |- F/_ x X   &    |- F/_ y Y   &    |- F/_ x A   &    |- F/_ y A   &    |- F/_ y B   &    |- F/_ x C   &    |- F/_ y C   &    |- F/_ x D   &    |- F/_ x F   &    |- F/_ y G   &    |- ( ( ph /\ y e. C ) -> X e. A )   &    |- ( ( ph /\ x e. A ) -> Y e. C )   &    |- ( ( ph /\ y e. C /\ x = X ) -> B = F )   &    |- ( ( ph /\ x e. A /\ y = Y ) -> D = G )   &    |- ( ( ph /\ x e. A ) -> B = G )   &    |- ( ( ph /\ y e. C ) -> D = F )   =>    |- ( ph -> U_ x e. A B = U_ y e. C D )
Theorem	cbviuneq12dv 35883*	Rule used to change the bound variables and classes in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by RP, 17-Jul-2020.)
|- ( ( ph /\ y e. C ) -> X e. A )   &    |- ( ( ph /\ x e. A ) -> Y e. C )   &    |- ( ( ph /\ y e. C /\ x = X ) -> B = F )   &    |- ( ( ph /\ x e. A /\ y = Y ) -> D = G )   &    |- ( ( ph /\ x e. A ) -> B = G )   &    |- ( ( ph /\ y e. C ) -> D = F )   =>    |- ( ph -> U_ x e. A B = U_ y e. C D )
Theorem	conrel1d 35884	Deduction about composition with a class with no relational content. (Contributed by Richard Penner, 24-Dec-2019.)
|- ( ph -> `' A = (/) )   =>    |- ( ph -> ( A o. B ) = (/) )
Theorem	conrel2d 35885	Deduction about composition with a class with no relational content. (Contributed by Richard Penner, 24-Dec-2019.)
|- ( ph -> `' A = (/) )   =>    |- ( ph -> ( B o. A ) = (/) )
21.25.2.1  Transitive relations (not to be confused with transitive classes).
Theorem	trrelind 35886	The intersection of transitive relations is a transitive relation. (Contributed by Richard Penner, 24-Dec-2019.)
|- ( ph -> ( R o. R ) C_ R )   &    |- ( ph -> ( S o. S ) C_ S )   &    |- ( ph -> T = ( R i^i S ) )   =>    |- ( ph -> ( T o. T ) C_ T )
Theorem	xpintrreld 35887	The intersection of a transitive relation with a cross product is a transitve relation. (Contributed by Richard Penner, 24-Dec-2019.)
|- ( ph -> ( R o. R ) C_ R )   &    |- ( ph -> S = ( R i^i ( A X. B ) ) )   =>    |- ( ph -> ( S o. S ) C_ S )
Theorem	restrreld 35888	The restriction of a transitive relation is a transitive relation. (Contributed by Richard Penner, 24-Dec-2019.)
|- ( ph -> ( R o. R ) C_ R )   &    |- ( ph -> S = ( R |` A ) )   =>    |- ( ph -> ( S o. S ) C_ S )
Theorem	trrelsuperreldg 35889	Concrete construction of a superclass of relation R which is a transitive relation. (Contributed by Richard Penner, 25-Dec-2019.)
|- ( ph -> Rel R )   &    |- ( ph -> S = ( dom R X. ran R ) )   =>    |- ( ph -> ( R C_ S /\ ( S o. S ) C_ S ) )
Theorem	trficl 35890*	The class of all transitive relations has the finite intersection property. (Contributed by Richard Penner, 1-Jan-2020.) (Proof shortened by Richard Penner, 3-Jan-2020.)
|- A = { z | ( z o. z ) C_ z }   =>    |- A. x e. A A. y e. A ( x i^i y ) e. A
Theorem	cnvtrrel 35891	The converse of a transitive relation is a transitive relation. (Contributed by Richard Penner, 25-Dec-2019.)
|- ( ( S o. S ) C_ S <-> ( `' S o. `' S ) C_ `' S )
Theorem	trrelsuperrel2dg 35892	Concrete construction of a superclass of relation R which is a transitive relation. (Contributed by RP, 20-Jul-2020.)
|- ( ph -> S = ( R u. ( dom R X. ran R ) ) )   =>    |- ( ph -> ( R C_ S /\ ( S o. S ) C_ S ) )
21.25.2.2  Reflexive closures
Syntax	crcl 35893	Extend class notation with reflexive closure.
class r*
Definition	df-rcl 35894*	Reflexive closure of a relation. This is the smallest superset which has the reflexive property. (Contributed by RP, 5-Jun-2020.)
|- r* = ( x e. _V |-> |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } )
Theorem	dfrcl2 35895	Reflexive closure of a relation as union with restricted identity relation. (Contributed by RP, 6-Jun-2020.)
|- r* = ( x e. _V |-> ( ( _I |` ( dom x u. ran x ) ) u. x ) )
Theorem	dfrcl3 35896	Reflexive closure of a relation as union of powers of the relation. (Contributed by RP, 6-Jun-2020.)
|- r* = ( x e. _V |-> ( ( x ^r 0 ) u. ( x ^r 1 ) ) )
Theorem	dfrcl4 35897*	Reflexive closure of a relation as indexed union of powers of the relation. (Contributed by RP, 8-Jun-2020.)
|- r* = ( r e. _V |-> U_ n e. { 0 , 1 } ( r ^r n ) )
21.25.2.3  Finite relationship composition. In order for theorems on the transitive closure of a relation to be grouped together before the concept of continuity, we really need an analogue of ^r that works on finite ordinals or finite sets instead of natural numbers.
Theorem	relexp2 35898	A set operated on by the relation exponent to the second power is equal to the composition of the set with itself. (Contributed by RP, 1-Jun-2020.)
|- ( R e. V -> ( R ^r 2 ) = ( R o. R ) )
Theorem	relexpnul 35899	If the domain and range of powers of a relation are disjoint then the relation raised to the sum of those exponents is empty. (Contributed by RP, 1-Jun-2020.)
|- ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> ( ( dom ( R ^r N ) i^i ran ( R ^r M ) ) = (/) <-> ( R ^r ( N + M ) ) = (/) ) )
Theorem	eliunov2 35900*	Membership in the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the the element is a member of that operator value. Generalized from dfrtrclrec2 13099. (Contributed by RP, 1-Jun-2020.)
|- C = ( r e. _V |-> U_ n e. N ( r .^ n ) )   =>    |- ( ( R e. U /\ N e. V ) -> ( X e. ( C ` R ) <-> E. n e. N X e. ( R .^ n ) ) )