P. 393 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39201-39300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnxrd 39201	A natural number is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. RR* )
Theorem	3adantll2 39202	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ( ph /\ et /\ ps ) /\ ch ) /\ th ) -> ta )
Theorem	3adantll3 39203	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ( ph /\ ps /\ et ) /\ ch ) /\ th ) -> ta )
Theorem	ssnel 39204	If not element of a set, then not element of a subset. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A C_ B /\ -. C e. B ) -> -. C e. A )
Theorem	jcn 39205	Inference joining the consequents of two premises. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ps )   &    |- ( ph -> -. ch )   =>    |- ( ph -> -. ( ps -> ch ) )
Theorem	elabrexg 39206*	Elementhood in an image set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( x e. A /\ B e. V ) -> B e. { y | E. x e. A y = B } )
Theorem	ifeq123d 39207	Equality deduction for conditional operator. (Contributed by Glauco Siliprandi, 11-Dec-2019.) AV: This theorem already exists as ifbieq12d 4113. TODO (NM): Please replace the usage of this theorem by ifbieq12d 4113 then delete this theorem. (New usage is discouraged.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> if ( ps , A , C ) = if ( ch , B , D ) )
Theorem	sncldre 39208	A singleton is closed w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR -> { A } e. ( Clsd ` ( topGen ` ran (,) ) ) )
Theorem	n0p 39209	A polynomial with a nonzero coefficient is not the zero polynomial. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ( P e. (Poly ` ZZ ) /\ N e. NN0 /\ ( (coeff ` P ) ` N ) =/= 0 ) -> P =/= 0p )
Theorem	pm2.65ni 39210	Inference rule for proof by contradiction. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( -. ph -> ps )   &    |- ( -. ph -> -. ps )   =>    |- ph
Theorem	pwssfi 39211	Every element of the power set of A is finite if and only if A is finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( A e. V -> ( A e. Fin <-> ~P A C_ Fin ) )
Theorem	iuneq2df 39212	Equality deduction for indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> U_ x e. A B = U_ x e. A C )
Theorem	nnfoctb 39213*	There exists a mapping from NN onto any (nonempty) countable set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( A ~<_ om /\ A =/= (/) ) -> E. f f : NN -onto-> A )
Theorem	ssinss1d 39214	Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A C_ C )   =>    |- ( ph -> ( A i^i B ) C_ C )
Theorem	0un 39215	The union of the empty set with a class is itself. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( (/) u. A ) = A
Theorem	elpwinss 39216	An element of the powerset of B intersected with anything, is a subset of B. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( A e. ( ~P B i^i C ) -> A C_ B )
Theorem	unidmex 39217	If F is a set, then U. dom F is a set (common case). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F e. V )   &    |- X = U. dom F   =>    |- ( ph -> X e. _V )
Theorem	ndisj2 39218*	A non disjointness condition. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( x = y -> B = C )   =>    |- ( -. Disj x e. A B <-> E. x e. A E. y e. A ( x =/= y /\ ( B i^i C ) =/= (/) ) )
Theorem	zenom 39219	The set of integer numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ZZ ~~ om
Theorem	rexsngf 39220*	Restricted existential quantification over a singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ps   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( E. x e. { A } ph <-> ps ) )
Theorem	uzwo4 39221*	Well-ordering principle: any nonempty subset of an upper set of integers has the least element. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ j ps   &    |- ( j = k -> ( ph <-> ps ) )   =>    |- ( ( S C_ ( ZZ>= ` M ) /\ E. j e. S ph ) -> E. j e. S ( ph /\ A. k e. S ( k < j -> -. ps ) ) )
Theorem	unisn0 39222	The union of the singleton of the empty set is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- U. { (/) } = (/)
Theorem	ssin0 39223	If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( ( A i^i B ) = (/) /\ C C_ A /\ D C_ B ) -> ( C i^i D ) = (/) )
Theorem	inabs3 39224	Absorption law for intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( C C_ B -> ( ( A i^i B ) i^i C ) = ( A i^i C ) )
Theorem	pwpwuni 39225	Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( A e. V -> ( A e. ~P ~P B <-> U. A e. ~P B ) )
Theorem	disjiun2 39226*	In a disjoint collection, an indexed union is disjoint from an additional term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> Disj x e. A B )   &    |- ( ph -> C C_ A )   &    |- ( ph -> D e. ( A \ C ) )   &    |- ( x = D -> B = E )   =>    |- ( ph -> ( U_ x e. C B i^i E ) = (/) )
Theorem	0pwfi 39227	The empty set is in any power set, and it's finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- (/) e. ( ~P A i^i Fin )
Theorem	ssinss2d 39228	Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> B C_ C )   =>    |- ( ph -> ( A i^i B ) C_ C )
Theorem	zct 39229	The set of integer numbers is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ZZ ~<_ om
Theorem	iunxsngf2 39230*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/_ x C   &    |- ( x = A -> B = C )   =>    |- ( A e. V -> U_ x e. { A } B = C )
Theorem	pwfin0 39231	A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ~P A i^i Fin ) =/= (/)
Theorem	uzct 39232	An upper integer set is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- Z = ( ZZ>= ` N )   =>    |- Z ~<_ om
Theorem	iunxsnf 39233*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/_ x C   &    |- A e. _V   &    |- ( x = A -> B = C )   =>    |- U_ x e. { A } B = C
Theorem	fiiuncl 39234*	If a set is closed under the union of two sets, then it is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. D )   &    |- ( ( ph /\ y e. D /\ z e. D ) -> ( y u. z ) e. D )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A =/= (/) )   =>    |- ( ph -> U_ x e. A B e. D )
Theorem	iunp1 39235*	The addition of the next set to a union indexed by a finite set of sequential integers. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/_ k B   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( k = ( N + 1 ) -> A = B )   =>    |- ( ph -> U_ k e. ( M ... ( N + 1 ) ) A = ( U_ k e. ( M ... N ) A u. B ) )
Theorem	fiunicl 39236*	If a set is closed under the union of two sets, then it is closed under finite union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( ph /\ x e. A /\ y e. A ) -> ( x u. y ) e. A )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A =/= (/) )   =>    |- ( ph -> U. A e. A )
Theorem	ixpeq2d 39237	Equality theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> X_ x e. A B = X_ x e. A C )
Theorem	disjxp1 39238*	The sets of a cartesian product are disjoint if the sets in the first argument are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> Disj x e. A B )   =>    |- ( ph -> Disj x e. A ( B X. C ) )
Theorem	disjsnxp 39239*	The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- Disj j e. A ( { j } X. B )
Theorem	eliind 39240*	Membership in indexed intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. |^|_ x e. B C )   &    |- ( ph -> K e. B )   &    |- ( x = K -> ( A e. C <-> A e. D ) )   =>    |- ( ph -> A e. D )
Theorem	rspcef 39241	Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- F/ x ps   &    |- F/_ x A   &    |- F/_ x B   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( ( A e. B /\ ps ) -> E. x e. B ph )
Theorem	inn0f 39242	A non-empty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( ( A i^i B ) =/= (/) <-> E. x e. A x e. B )
Theorem	ixpssmapc 39243*	An infinite Cartesian product is a subset of set exponentiation. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- F/ x ph   &    |- ( ph -> C e. V )   &    |- ( ( ph /\ x e. A ) -> B C_ C )   =>    |- ( ph -> X_ x e. A B C_ ( C ^m A ) )
Theorem	inn0 39244*	A non-empty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ( A i^i B ) =/= (/) <-> E. x e. A x e. B )
Theorem	elintd 39245*	Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. B ) -> A e. x )   =>    |- ( ph -> A e. |^| B )
Theorem	eqneltri 39246	If a class is not an element of another class, an equal class is also not an element. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- A = B   &    |- -. B e. C   =>    |- -. A e. C
Theorem	ssdf 39247*	A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> x e. B )   =>    |- ( ph -> A C_ B )
Theorem	brneqtrd 39248	Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> -. A R B )   &    |- ( ph -> B = C )   =>    |- ( ph -> -. A R C )
Theorem	ssnct 39249	A set containing an uncountable set is itself uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> -. A ~<_ om )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> -. B ~<_ om )
Theorem	ssuniint 39250*	Sufficient condition for being a subclass of the union of an intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. B ) -> A e. x )   =>    |- ( ph -> A C_ U. |^| B )
Theorem	elintdv 39251*	Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ x e. B ) -> A e. x )   =>    |- ( ph -> A e. |^| B )
Theorem	ssd 39252*	A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ( ph /\ x e. A ) -> x e. B )   =>    |- ( ph -> A C_ B )
Theorem	ralimralim 39253	Introducing any antecedent in a restricted universal quantification. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( A. x e. A ph -> A. x e. A ( ps -> ph ) )
Theorem	snelmap 39254	Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> ( A X. { x } ) e. ( B ^m A ) )   =>    |- ( ph -> x e. B )
Theorem	dfcleqf 39255	Equality connective between classes. Same as dfcleq 2616, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
Theorem	xrnmnfpnf 39256	An extended real that is neither real nor minus infinity, is plus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> -. A e. RR )   &    |- ( ph -> A =/= -oo )   =>    |- ( ph -> A = +oo )
Theorem	nelrnmpt 39257*	Non-membership in the range of a function in maps-to notaion. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/ x ph   &    |- F = ( x e. A |-> B )   &    |- ( ph -> C e. V )   &    |- ( ( ph /\ x e. A ) -> C =/= B )   =>    |- ( ph -> -. C e. ran F )
Theorem	snn0d 39258	The singleton of a set is not empty. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   =>    |- ( ph -> { A } =/= (/) )
Theorem	iuneq1i 39259*	Equality theorem for indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- A = B   =>    |- U_ x e. A C = U_ x e. B C
Theorem	nssrex 39260*	Negation of subclass relationship. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( -. A C_ B <-> E. x e. A -. x e. B )
Theorem	nelpr2 39261	If a class is not an element of an unordered pair, it is not the second listed element. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> -. A e. { B , C } )   =>    |- ( ph -> A =/= C )
Theorem	nelpr1 39262	If a class is not an element of an unordered pair, it is not the first listed element. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> -. A e. { B , C } )   =>    |- ( ph -> A =/= B )
Theorem	iunssf 39263	Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/_ x C   =>    |- ( U_ x e. A B C_ C <-> A. x e. A B C_ C )
Theorem	ssinc 39264*	Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ m e. ( M..^ N ) ) -> ( F ` m ) C_ ( F ` ( m + 1 ) ) )   =>    |- ( ph -> ( F ` M ) C_ ( F ` N ) )
Theorem	ssdec 39265*	Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ m e. ( M..^ N ) ) -> ( F ` ( m + 1 ) ) C_ ( F ` m ) )   =>    |- ( ph -> ( F ` N ) C_ ( F ` M ) )
Theorem	elixpconstg 39266*	Membership in an infinite Cartesian product of a constant B. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( F e. V -> ( F e. X_ x e. A B <-> F : A --> B ) )
Theorem	iineq1d 39267*	Equality theorem for indexed intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> A = B )   =>    |- ( ph -> |^|_ x e. A C = |^|_ x e. B C )
Theorem	metpsmet 39268	A metric is a pseudometric. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( D e. ( Met ` X ) -> D e. (PsMet ` X ) )
Theorem	ixpssixp 39269	Subclass theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B C_ C )   =>    |- ( ph -> X_ x e. A B C_ X_ x e. A C )
Theorem	ballss3 39270*	A sufficient condition for a ball being a subset. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ x ph   &    |- ( ph -> D e. (PsMet ` X ) )   &    |- ( ph -> P e. X )   &    |- ( ph -> R e. RR* )   &    |- ( ( ph /\ x e. X /\ ( P D x ) < R ) -> x e. A )   =>    |- ( ph -> ( P ( ball ` D ) R ) C_ A )
Theorem	iunssd 39271*	Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ( ph /\ x e. A ) -> B C_ C )   =>    |- ( ph -> U_ x e. A B C_ C )
Theorem	iunincfi 39272*	Given a sequence of increasing sets, the union of a finite subsequence, is its last element. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ n e. ( M..^ N ) ) -> ( F ` n ) C_ ( F ` ( n + 1 ) ) )   =>    |- ( ph -> U_ n e. ( M ... N ) ( F ` n ) = ( F ` N ) )
Theorem	nsstr 39273	If it's not a subclass, it's not a subclass of a smaller one. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ( -. A C_ B /\ C C_ B ) -> -. A C_ C )
Theorem	rabbida 39274	Equivalent wff's yield equal restricted class abstractions (deduction rule). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> { x e. A | ps } = { x e. A | ch } )
Theorem	rexanuz3 39275*	Combine two different upper integer properties into one, for a single integer. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ j ph   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ch )   &    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ps )   &    |- ( k = j -> ( ch <-> th ) )   &    |- ( k = j -> ( ps <-> ta ) )   =>    |- ( ph -> E. j e. Z ( th /\ ta ) )
Theorem	rabeqd 39276*	Equality theorem for restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A = B )   =>    |- ( ph -> { x e. A | ch } = { x e. B | ch } )
Theorem	cbvmpt22 39277*	Rule to change the second bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/_ y A   &    |- F/_ w A   &    |- F/_ w C   &    |- F/_ y E   &    |- ( y = w -> C = E )   =>    |- ( x e. A , y e. B |-> C ) = ( x e. A , w e. B |-> E )
Theorem	cbvmpt21 39278*	Rule to change the first bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/_ x B   &    |- F/_ z B   &    |- F/_ z C   &    |- F/_ x E   &    |- ( x = z -> C = E )   =>    |- ( x e. A , y e. B |-> C ) = ( z e. A , y e. B |-> E )
Theorem	eliuniin 39279*	Indexed union of indexed intersections. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- A = U_ x e. B |^|_ y e. C D   =>    |- ( Z e. V -> ( Z e. A <-> E. x e. B A. y e. C Z e. D ) )
Theorem	ssabf 39280	Subclass of a class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/_ x A   =>    |- ( A C_ { x | ph } <-> A. x ( x e. A -> ph ) )
Theorem	uniexd 39281	Deduction version of the ZF Axiom of Union in class notation. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. V )   =>    |- ( ph -> U. A e. _V )
Theorem	pwexd 39282	Deduction version of the power set axiom. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. V )   =>    |- ( ph -> ~P A e. _V )
Theorem	pssnssi 39283	A proper subclass does not include the other class. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- A C. B   =>    |- -. B C_ A
Theorem	rabidim2 39284	Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( x e. { x e. A | ph } -> ph )
Theorem	xpexd 39285	The Cartesian product of two sets is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> ( A X. B ) e. _V )
Theorem	eluni2f 39286*	Membership in class union. Restricted quantifier version. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A e. U. B <-> E. x e. B A e. x )
Theorem	eliin2f 39287*	Membership in indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/_ x B   =>    |- ( B =/= (/) -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )
Theorem	nssd 39288	Negation of subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> X e. A )   &    |- ( ph -> -. X e. B )   =>    |- ( ph -> -. A C_ B )
Theorem	iineq12dv 39289*	Equality deduction for indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A = B )   &    |- ( ( ph /\ x e. B ) -> C = D )   =>    |- ( ph -> |^|_ x e. A C = |^|_ x e. B D )
Theorem	supxrcld 39290	The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A C_ RR* )   =>    |- ( ph -> sup ( A , RR* , < ) e. RR* )
Theorem	elrestd 39291	A sufficient condition for being an open set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> J e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> X e. J )   &    |- A = ( X i^i B )   =>    |- ( ph -> A e. ( J ↾t B ) )
Theorem	eliuniincex 39292*	Counterexample to show that the additional conditions in eliuniin 39279 and eliuniin2 39303 are actually needed. Notice that the definition of A is not even needed (it can be any class). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- B = { (/) }   &    |- C = (/)   &    |- D = (/)   &    |- Z = _V   =>    |- -. ( Z e. A <-> E. x e. B A. y e. C Z e. D )
Theorem	eliincex 39293*	Counterexample to show that the additional conditions in eliin 4525 and eliin2 39299 are actually needed. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- A = _V   &    |- B = (/)   =>    |- -. ( A e. |^|_ x e. B C <-> A. x e. B A e. C )
Theorem	eliinid 39294*	Membership in an indexed intersection implies membership in any intersected set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ( A e. |^|_ x e. B C /\ x e. B ) -> A e. C )
Theorem	abssf 39295	Class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/_ x A   =>    |- ( { x | ph } C_ A <-> A. x ( ph -> x e. A ) )
Theorem	fexd 39296	If the domain of a mapping is a set, the function is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> F : A --> B )   &    |- ( ph -> A e. C )   =>    |- ( ph -> F e. _V )
Theorem	supxrubd 39297	A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A C_ RR* )   &    |- ( ph -> B e. A )   &    |- S = sup ( A , RR* , < )   =>    |- ( ph -> B <_ S )
Theorem	ssrabf 39298	Subclass of a restricted class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/_ x B   &    |- F/_ x A   =>    |- ( B C_ { x e. A | ph } <-> ( B C_ A /\ A. x e. B ph ) )
Theorem	eliin2 39299*	Membership in indexed intersection. See eliincex 39293 for a counterexample showing that the precondition B =/= (/) cannot be simply dropped. eliin 4525 uses an alternative precondition (and it doesn't have a disjoint var constraint between B and x; see eliin2f 39287). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( B =/= (/) -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )
Theorem	ssrab2f 39300	Subclass relation for a restricted class. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/_ x A   =>    |- { x e. A | ph } C_ A