Most Recent Proofs - Intuitionistic Logic Explorer

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

Last updated on 15-Aug-2026 at 6:58 AM ET.

Recent Additions to the Intuitionistic Logic Explorer

Date	Label	Description
Theorem
6-Aug-2026	relndmfv 5728	The value of a relation outside its domain is the empty set. (Contributed by Jim Kingdon, 6-Aug-2026.)
|- ( ( Rel F /\ -. A e. dom F ) -> ( F ` A ) = (/) )
1-Aug-2026	wexmiddifxy 17046	Being able to subtract an arbitrary finite set from a finite set and get a finite set is equivalent to weak excluded middle. By adding additional conditions we can get a theorem which does not need weak excluded middle, at diffifi 7198. (Contributed by Jim Kingdon, 1-Aug-2026.)
|- (WEXMID <-> A. x A. y ( ( x e. Fin /\ y e. Fin ) -> ( x \ y ) e. Fin ) )
1-Aug-2026	wexmiddifxylem 17045	Lemma for wexmiddifxylem 17045. Showing weak excluded middle given a suitable finite set. (Contributed by Jim Kingdon, 1-Aug-2026.)
|- ( ( { 1o } \ { { x e. 1o | ph } } ) e. Fin -> DECID -. ph )
31-Jul-2026	rabid1o 17034	Converting between propositions and corresponding subsets of a singleton. (Contributed by Jim Kingdon, 31-Jul-2026.)
|- ( { x e. 1o | ph } = 1o <-> ph )
30-Jul-2026	wexmiddc 17042	Weak excluded middle expressed using WEXMID implies decidability of a negated proposition. (Contributed by Jim Kingdon, 30-Jul-2026.)
|- (WEXMID -> DECID -. ph )
30-Jul-2026	df-wexmid 17041	Weak excluded middle is the principle that any negated proposition is decidable. (Contributed by Jim Kingdon, 30-Jul-2026.)
|- (WEXMID <-> A. p e. ~P 1o ( -. p = 1o \/ -. -. p = 1o ) )
29-Jul-2026	wexmiddiffi 17044	Being able to subtract an arbitrary set from a finite set and get a finite set is equivalent to weak excluded middle. By adding additional conditions we can get a theorem which does not need weak excluded middle, at diffifi 7198. (Contributed by Jim Kingdon, 29-Jul-2026.)
|- (WEXMID <-> A. x A. y ( x e. Fin -> ( x \ y ) e. Fin ) )
29-Jul-2026	wexmiddiffilem 17043	Lemma for wexmiddiffi 17044. The reverse direction, using different notation. (Contributed by Jim Kingdon, 29-Jul-2026.)
|- ( A. x A. y ( x e. Fin -> ( x \ y ) e. Fin ) -> ( -. ph \/ -. -. ph ) )
24-Jul-2026	stnot 17039	A proposition is double negation stable if and only if it is equivalent to a negated proposition. Here by "proposition" we mean a subset of a singleton (which is a choice which allows us to quantify over them). Posed as an exercise online by Yannick Forster. (Contributed by Jim Kingdon, 24-Jul-2026.)
|- ( A e. ~P 1o -> ( ( -. -. A = 1o -> A = 1o ) <-> E. y e. ~P 1o ( A = 1o <-> -. y = 1o ) ) )
24-Jul-2026	slotm 13415	A structure with an inhabited slot is inhabited. (Contributed by Jim Kingdon, 24-Jul-2026.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   =>    |- ( A e. ( E ` G ) -> E. j j e. G )
22-Jul-2026	alseu-no-surprise 17179	Demonstrate that there is never a "surprise" when using the "all some one" quantifier, that is, it is never possible for the consequent to be both always true and always false. This follows from als-no-surprise 17147 by alseuals 17165. See als-no-surprise 17147 for why ordinary "for all" with implication has no such property. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- -. ( A.E! x ( ph -> ps ) /\ A.E! x ( ph -> -. ps ) )
22-Jul-2026	alseueu 17178	"The ph is ps " implies that exactly one thing is both ph and ps. This is the half of dfalseu2 17177 that drops the universal conjunct; it does not reverse, so E! x ( ph /\ ps ) cannot be used in place of an "all some one" statement. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x ( ph -> ps ) -> E! x ( ph /\ ps ) )
22-Jul-2026	dfalseu2 17177	An "all some one" statement is equivalent to its universal part conjoined with the claim that exactly one x satisfies both ph and ps. In other words, given A. x ( ph -> ps ), requiring exactly one x to satisfy ph, which is what df-alseu 17162 requires, and requiring exactly one x to satisfy ( ph /\ ps ) come to the same thing. Read ph as "is a king" and ps as "is hungry": if every king is hungry, then "there is exactly one king" and "there is exactly one hungry king" say the same thing, so either of them, together with "every king is hungry", gives "the king is hungry". The universal conjunct is what makes that work, and it cannot be dropped. E! x ( ph /\ ps ) on its own is strictly weaker than A.E! x ( ph -> ps ), since it is satisfied when many things are ph and just one of those is ps, as in a region with five kings exactly one of whom is hungry; see alseueu 17178 for the one direction that does hold without it. Uniqueness attaches to the antecedent, not to the conjunction. Russell's analysis of a definite description is built the same way: its uniqueness clause constrains the description predicate alone, while the predication is a separate conjunct. See his worked example of "the father of Charles II was executed", [Russell1905] p. 482. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ( ph /\ ps ) ) )
22-Jul-2026	nfralseu 17176	Bound-variable hypothesis builder for "all some one" restricted to a class. This is the "all some one" counterpart of nfrals 17145. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- F/_ x A   &    |- F/ x ph   &    |- F/ x ps   =>    |- F/ x A.E! y e. A ( ph -> ps )
22-Jul-2026	nfalseu 17175	Bound-variable hypothesis builder for "all some one". This is the "all some one" counterpart of nfals 17144. Unlike the set.mm version of this theorem, no disjoint variable condition is needed, because nfeu 2105 here does not require one. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x A.E! y ( ph -> ps )
22-Jul-2026	ralseubii 17174	Congruence for "all some one" restricted to a class. This is the "all some one" counterpart of ralsbii 17142. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph <-> ch )   &    |- ( ps <-> th )   =>    |- ( A.E! x e. A ( ph -> ps ) <-> A.E! x e. A ( ch -> th ) )
22-Jul-2026	alseubii 17173	Congruence: equivalents may be substituted inside an "all some one". This is the "all some one" counterpart of alsbii 17141. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph <-> ch )   &    |- ( ps <-> th )   =>    |- ( A.E! x ( ph -> ps ) <-> A.E! x ( ch -> th ) )
22-Jul-2026	ralseu2d 17172	Deduction rule: Given "all some one" applied to a class, you can extract the "exactly one" part. Note that the witness must satisfy the antecedent ps, not merely be a member of A. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph -> A.E! x e. A ( ps -> ch ) )   =>    |- ( ph -> E! x e. A ps )
22-Jul-2026	ralseu1d 17171	Deduction rule: Given "all some one" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph -> A.E! x e. A ( ps -> ch ) )   =>    |- ( ph -> A. x e. A ( ps -> ch ) )
22-Jul-2026	alseu2d 17170	Deduction rule: Given "all some one" applied to a top-level inference, you can extract the "exactly one" part. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph -> A.E! x ( ps -> ch ) )   =>    |- ( ph -> E! x ps )
22-Jul-2026	alseu1d 17169	Deduction rule: Given "all some one" applied to a top-level inference, you can extract the "for all" part. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph -> A.E! x ( ps -> ch ) )   =>    |- ( ph -> A. x ( ps -> ch ) )
22-Jul-2026	ralseud 17168	Introduction rule for "all some one" restricted to a class. This is the converse of ralseu1d 17171 and ralseu2d 17172 taken together. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph -> A. x e. A ( ps -> ch ) )   &    |- ( ph -> E! x e. A ps )   =>    |- ( ph -> A.E! x e. A ( ps -> ch ) )
22-Jul-2026	alseud 17167	Introduction rule: "all some one" holds if the "for all" part holds and the antecedent has exactly one witness. This is the converse of alseu1d 17169 and alseu2d 17170 taken together. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph -> A. x ( ps -> ch ) )   &    |- ( ph -> E! x ps )   =>    |- ( ph -> A.E! x ( ps -> ch ) )
22-Jul-2026	ralseurals 17166	"All some one" restricted to a class implies "all some" restricted to that class. Restricted counterpart of alseuals 17165. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x e. A ( ph -> ps ) -> A.E. x e. A ( ph -> ps ) )
22-Jul-2026	alseuals 17165	"All some one" implies "all some": requiring exactly one witness is stronger than requiring at least one. Any consequence of an allsome statement is therefore a consequence of the corresponding "all some one" statement, which is how alseu-no-surprise 17179 is proved. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x ( ph -> ps ) -> A.E. x ( ph -> ps ) )
22-Jul-2026	dfralseu2 17164	The bounded "all some one" form is the general form with the class membership folded into the antecedent. This is the "all some one" counterpart of dfrals2 17130. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x e. A ( ph -> ps ) <-> A.E! x ( ( x e. A /\ ph ) -> ps ) )
22-Jul-2026	df-ralseu 17163	Define "all some one" applied to a class, which means ps is true whenever ph is true for x in A, and exactly one x in A satisfies ph. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )
22-Jul-2026	df-alseu 17162	Define "all some one" applied to a top-level implication, which means ps is true whenever ph is true and exactly one x satisfies ph. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )
22-Jul-2026	wralseu 17161	Extend wff definition to include "all some one" applied to a class, which means ps is true whenever ph is true for x in A, and exactly one x in A satisfies ph. (Contributed by David A. Wheeler, 22-Jul-2026.)
wff A.E! x e. A ( ph -> ps )
22-Jul-2026	walseu 17160	Extend wff definition to include "all some one" applied to a top-level implication, which means ps is true whenever ph is true, and exactly one x satisfies ph. (Contributed by David A. Wheeler, 22-Jul-2026.)
wff A.E! x ( ph -> ps )
22-Jul-2026	mptmex 5945	If a function given by maps-to notation is inhabited, then the class it is defined on is inhabited. (Contributed by Jim Kingdon, 22-Jul-2026.)
|- ( C e. ( x e. A |-> B ) -> E. y y e. A )
20-Jul-2026	2alsraln0idm 17159	Nested general "all some" quantifiers with class membership as their antecedents, for the same class A: ph holds for every x and every y in A, and A is inhabited. (Contributed by Peter Mazsa, 28-May-2019.) (Revised by David A. Wheeler, 20-Jul-2026.)
|- ( A.E. x ( x e. A -> A.E. y ( y e. A -> ph ) ) <-> ( A. x e. A A. y e. A ph /\ E. x x e. A ) )
20-Jul-2026	2alsraln0m 17158	Nested general "all some" quantifiers with class membership as their antecedents: ph holds for every x in A and every y in B, and both A and B are inhabited. (Contributed by Peter Mazsa, 28-May-2019.) (Revised by David A. Wheeler, 20-Jul-2026.)
|- ( A.E. x ( x e. A -> A.E. y ( y e. B -> ph ) ) <-> ( A. x e. A A. y e. B ph /\ ( E. x x e. A /\ E. y y e. B ) ) )
20-Jul-2026	n0alsm 17157	If A is inhabited, then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that ph holds for every x in A. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
|- ( E. x x e. A -> ( A.E. x ( x e. A -> ph ) <-> A. x e. A ph ) )
20-Jul-2026	alsraln0m 17154	The general "all some" quantifier with class membership as its antecedent holds if and only if ph holds for every x in A and A is inhabited. This is the intuitionistic form of what set.mm states using A =/= (/); see the section comment. (Contributed by Peter Mazsa, 28-Nov-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
|- ( A.E. x ( x e. A -> ph ) <-> ( A. x e. A ph /\ E. x x e. A ) )
20-Jul-2026	alsralrex 17153	The general "all some" quantifier with class membership as its antecedent holds if and only if ph holds for every x in A and some x in A satisfies ph. (Contributed by Peter Mazsa, 27-Nov-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
|- ( A.E. x ( x e. A -> ph ) <-> ( A. x e. A ph /\ E. x e. A ph ) )
20-Jul-2026	ralsanmo 17152	An "all some" statement restricted to a class, conjoined with the claim that at most one x in A satisfies its antecedent, is equivalent to the universal part conjoined with the claim that exactly one x in A satisfies the antecedent. This is the restricted counterpart of alsanmo 17151. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
|- ( ( A.E. x e. A ( ph -> ps ) /\ E* x e. A ph ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )
20-Jul-2026	alsanmo 17151	An "all some" statement conjoined with the claim that at most one x satisfies its antecedent is equivalent to the universal part conjoined with the claim that exactly one x satisfies the antecedent. The "all some" quantifier supplies the existence of such an x and E* x ph supplies the at-most-one part, so together they yield E! x ph. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
|- ( ( A.E. x ( ph -> ps ) /\ E* x ph ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )
20-Jul-2026	rexrals 17150	If a member of A satisfying the antecedent exists, then a restricted "all some" statement reduces to its universal part. This is the restricted counterpart of rexals 17156. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
|- ( E. x e. A ph -> ( A.E. x e. A ( ph -> ps ) <-> A. x e. A ( ph -> ps ) ) )
20-Jul-2026	ralrals 17149	If the universal part of a restricted "all some" statement holds, then the statement reduces to the existence of a member of A satisfying its antecedent. This is the restricted counterpart of ralals 17155. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
|- ( A. x e. A ( ph -> ps ) -> ( A.E. x e. A ( ph -> ps ) <-> E. x e. A ph ) )
20-Jul-2026	als-no-surprise 17147	Demonstrate that there is never a "surprise" when using the allsome quantifier, that is, it is never possible for the consequent to be both always true and always false. This uses the definition of df-als 17128: the universal parts give A. x -. ph, which contradicts the witness that the allsome quantifier supplies. Ordinary "for all" with implication has no such property, since A. x ( ph -> ps ) and A. x ( ph -> -. ps ) can both hold when nothing satisfies ph. (Contributed by David A. Wheeler, 27-Oct-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
|- -. ( A.E. x ( ph -> ps ) /\ A.E. x ( ph -> -. ps ) )
20-Jul-2026	ralsmd 17138	Deduction rule: Given "all some" applied to a class, the class is inhabited. This is stronger than ralsn0d 17137, which only concludes that the class is nonempty; see n0r 3535. (Contributed by David A. Wheeler, 20-Jul-2026.)
|- ( ph -> A.E. x e. A ( ps -> ch ) )   =>    |- ( ph -> E. x x e. A )
19-Jul-2026	disjdifg 3598	A class and its relative complement are disjoint. (Contributed by NM, 24-Mar-1998.) Generalize from disjdif 3599. (Revised by BJ, 19-Jul-2026.)
|- ( A C_ B -> ( A i^i ( C \ B ) ) = (/) )
19-Jul-2026	sseq0b 3564	The only subclass of the empty class is itself. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Strengthen sseq0 3565 to a biconditional. (Revised by BJ, 19-Jul-2026.)
|- ( A = (/) -> ( B C_ A <-> B = (/) ) )
18-Jul-2026	sepab 4278	Separation Scheme (Aussonderung) in terms of a class abstraction. Prefer using the more natural statement rabexg 4279. (Contributed by NM, 8-Jun-1994.) Put in closed form. (Revised by BJ, 18-Jul-2026.)
|- ( A e. V -> { x | ( x e. A /\ ph ) } e. _V )
18-Jul-2026	inssdif0im 3592	Intersection, subclass, and difference relationship. The converse holds in classical logic but not in intuitionistic logic. (Contributed by Jim Kingdon, 3-Aug-2018.) (Proof shortened by BJ, 18-Jul-2026.)
|- ( ( A i^i B ) C_ C -> ( A i^i ( B \ C ) ) = (/) )
15-Jul-2026	rexals 17156	If some x in A satisfies ph, then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that ph holds for every x in A. See rexrals 17150 for the restricted counterpart. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)
|- ( E. x e. A ph -> ( A.E. x ( x e. A -> ph ) <-> A. x e. A ph ) )
15-Jul-2026	ralals 17155	If ph holds for every x in A, then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that some x in A satisfies ph. See ralrals 17149 for the restricted counterpart. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)
|- ( A. x e. A ph -> ( A.E. x ( x e. A -> ph ) <-> E. x e. A ph ) )
14-Jul-2026	uniex2 4581	The Axiom of Union using the standard abbreviation for union. Given any set x, its union y exists. (Contributed by NM, 4-Jun-2006.) (Proof shortened by BJ, 14-Jul-2026.)
|- E. y y = U. x
14-Jul-2026	sepgi 4252	Inference associated with sepg 4251. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 14-Jul-2026.)
|- A e. _V   =>    |- E. y A. x ( x e. y <-> ( x e. A /\ ph ) )
13-Jul-2026	f1setfi 7317	The set of injections between two finite sets is finite. (Contributed by Jim Kingdon, 13-Jul-2026.)
|- ( ( A e. Fin /\ B e. Fin ) -> { f | f : A -1-1-> B } e. Fin )
13-Jul-2026	fdcf1 7316	It is decidable whether a function from a finite set into another finite set is one-to-one. (Contributed by Jim Kingdon, 13-Jul-2026.)
|- ( ( A e. Fin /\ B e. Fin /\ F : A --> B ) -> DECID F : A -1-1-> B )
12-Jul-2026	rals-no-surprise 17148	Demonstrate that there is never a "surprise" when using the allsome quantifier restricted to a class, that is, it is never possible for the consequent to be both always true and always false of the members of A that satisfy the antecedent. This is the restricted counterpart of als-no-surprise 17147, and follows from it by dfrals2 17130. Note that this holds without any assumption that A is inhabited; that is the point of allsome, since the corresponding claim for the ordinary restricted "for all" fails when nothing in A satisfies ph. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- -. ( A.E. x e. A ( ph -> ps ) /\ A.E. x e. A ( ph -> -. ps ) )
12-Jul-2026	cbvals 17146	Rule used to change bound variables, using implicit substitution. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( x = y -> ( ph <-> ch ) )   &    |- ( x = y -> ( ps <-> th ) )   =>    |- ( A.E. x ( ph -> ps ) <-> A.E. y ( ch -> th ) )
12-Jul-2026	nfrals 17145	Bound-variable hypothesis builder for "all some" restricted to a class. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- F/_ x A   &    |- F/ x ph   &    |- F/ x ps   =>    |- F/ x A.E. y e. A ( ph -> ps )
12-Jul-2026	nfals 17144	Bound-variable hypothesis builder for "all some". (Contributed by David A. Wheeler, 12-Jul-2026.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x A.E. y ( ph -> ps )
12-Jul-2026	alsbid 17143	Deduction form of alsbii 17141. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- F/ x ph   &    |- ( ph -> ( ps <-> th ) )   &    |- ( ph -> ( ch <-> ta ) )   =>    |- ( ph -> ( A.E. x ( ps -> ch ) <-> A.E. x ( th -> ta ) ) )
12-Jul-2026	ralsbii 17142	Congruence for "all some" restricted to a class. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( ph <-> ch )   &    |- ( ps <-> th )   =>    |- ( A.E. x e. A ( ph -> ps ) <-> A.E. x e. A ( ch -> th ) )
12-Jul-2026	alsbii 17141	Congruence: equivalents may be substituted inside an "all some". (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( ph <-> ch )   &    |- ( ps <-> th )   =>    |- ( A.E. x ( ph -> ps ) <-> A.E. x ( ch -> th ) )
12-Jul-2026	ralsex 17140	The consequent of an "all some" restricted to a class is witnessed: some member of A satisfying ph also satisfies ps. Restricted counterpart of alsex 17139. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( A.E. x e. A ( ph -> ps ) -> E. x e. A ps )
12-Jul-2026	alsex 17139	The consequent of an "all some" is witnessed: if ps holds of every x satisfying ph, and some x satisfies ph, then some x satisfies ps. This is the positive counterpart of als-no-surprise 17147, and it is the property that ordinary "for all" with implication lacks: from A. x ( ph -> ps ) alone nothing whatever follows about ps, since nothing need satisfy ph. It is the allsome quantifier says what a speaker of "all Martians are green" usually means. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( A.E. x ( ph -> ps ) -> E. x ps )
12-Jul-2026	ralsn0d 17137	Deduction rule: Given "all some" applied to a class, the class is not the empty set. (Contributed by David A. Wheeler, 23-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
|- ( ph -> A.E. x e. A ( ps -> ch ) )   =>    |- ( ph -> A =/= (/) )
12-Jul-2026	rals2d 17136	Deduction rule: Given "all some" applied to a class, you can extract the "there exists" part. Note that the witness must satisfy the antecedent ps, not merely be a member of A. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
|- ( ph -> A.E. x e. A ( ps -> ch ) )   =>    |- ( ph -> E. x e. A ps )
12-Jul-2026	rals1d 17135	Deduction rule: Given "all some" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
|- ( ph -> A.E. x e. A ( ps -> ch ) )   =>    |- ( ph -> A. x e. A ( ps -> ch ) )
12-Jul-2026	ralsd 17132	Introduction rule for "all some" restricted to a class. This is the converse of rals1d 17135 and rals2d 17136 taken together. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( ph -> A. x e. A ( ps -> ch ) )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> A.E. x e. A ( ps -> ch ) )
12-Jul-2026	alsd 17131	Introduction rule: "all some" holds if the "for all" part holds and the antecedent has a witness. This is the converse of als1d 17133 and als2d 17134 taken together, and is what lets an "all some" statement be proved rather than merely taken apart. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( ph -> A. x ( ps -> ch ) )   &    |- ( ph -> E. x ps )   =>    |- ( ph -> A.E. x ( ps -> ch ) )
12-Jul-2026	dfrals2 17130	The bounded "all some" form is the general form with the class membership folded into the antecedent. (Contributed by David A. Wheeler, 22-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
|- ( A.E. x e. A ( ph -> ps ) <-> A.E. x ( ( x e. A /\ ph ) -> ps ) )
12-Jul-2026	df-rals 17129	Define "all some" applied to a class, which means ps is true whenever ph is true for x in A, and there is at least one x in A where ph is true. An older definition of the "all some" quantifier when scoped to a class, named df-alsc and now removed, instead applied a bare formula ph to the members of a class, asserting only ( A. x e. A ph /\ E. x x e. A ), that is, that the formula held throughout A and that A had at least one member. I've now decided that that was a mistake. Its older existence conjunct E. x x e. A did not require any member of A to satisfy the antecedent, so if the formula was itself an implication, that inner implication could still be vacuously true, which is precisely what the allsome quantifier exists to prevent. For example, the older definition meant that "among Martians, all tall ones are green" could be considered true if there are Martians, but no tall Martians. This version of the definition instead ensures that claims of the form "among Martians, all tall ones are green" can only be true if all tall Martians are green and that there is at least one tall Martian. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
|- ( A.E. x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) )
12-Jul-2026	wrals 17127	Extend wff definition to include "all some" applied to a class, which means ps is true whenever ph is true for x in A, and there is at least one x in A where ph is true. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
wff A.E. x e. A ( ph -> ps )
12-Jul-2026	wals 17126	Extend wff definition to include "all some" applied to a top-level implication, which means ps is true whenever ph is true, and there is at least one x where ph is true. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
wff A.E. x ( ph -> ps )
12-Jul-2026	vvin 3569	Two classes are both the universal class if and only if their intersection is the universal class. Dual of un00 3567. (Contributed by BJ, 12-Jul-2026.)
|- ( ( A = _V /\ B = _V ) <-> ( A i^i B ) = _V )
7-Jul-2026	cmnsubm 14112	A submonoid of a commutative monoid is commutative. (Contributed by Jim Kingdon, 7-Jul-2026.)
|- ( ph -> S e. (SubMnd ` G ) )   &    |- ( ph -> G e. CMnd )   &    |- H = ( G ↾s S )   =>    |- ( ph -> H e. CMnd )
29-Jun-2026	dichmul0or 16760	Real number dichotomy is equivalent to the zero product principle for complex numbers: if a product is zero, one of its factors must be zero. (Contributed by Matthew House, 29-Jun-2026.)
|- ( A. x e. RR A. y e. RR ( x <_ y \/ y <_ x ) <-> A. z e. CC A. w e. CC ( ( z x. w ) = 0 -> ( z = 0 \/ w = 0 ) ) )
29-Jun-2026	dichmul0orlem5 16757	Lemma for dichmul0or 16760. (Contributed by Matthew House, 29-Jun-2026.)
|- ( ph -> A e. RR )   &    |- ( ph -> ( ( abs ` A ) + A ) = 0 )   =>    |- ( ph -> A <_ 0 )
29-Jun-2026	dichmul0orlem4 16756	Lemma for dichmul0or 16760. (Contributed by Matthew House, 29-Jun-2026.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( ( ( abs ` A ) + A ) x. ( ( abs ` A ) - A ) ) = 0 )
29-Jun-2026	dichmul0orlem3 16755	Lemma for dichmul0or 16760. (Contributed by Matthew House, 29-Jun-2026.)
|- ( ph -> A. x e. RR A. y e. RR ( x <_ y \/ y <_ x ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A x. B ) = 0 )   =>    |- ( ph -> ( A = 0 \/ B = 0 ) )
29-Jun-2026	dichmul0orlem2 16754	Lemma for dichmul0or 16760. (Contributed by Matthew House, 29-Jun-2026.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A x. B ) = 0 )   &    |- ( ph -> ( abs ` A ) <_ ( abs ` B ) )   =>    |- ( ph -> A = 0 )
29-Jun-2026	dichmul0orlem1 16753	Lemma for dichmul0or 16760. (Contributed by Matthew House, 29-Jun-2026.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( A x. B ) = 0 )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> A = 0 )
29-Jun-2026	lealltlt2 16752	Alternative definition for <_ on real numbers. (Contributed by Matthew House, 29-Jun-2026.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> A. x e. RR ( B < x -> A < x ) ) )
29-Jun-2026	lealltlt1 16751	Alternative definition for <_ on real numbers. (Contributed by Matthew House, 29-Jun-2026.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> A. x e. RR ( x < A -> x < B ) ) )
28-Jun-2026	dichmul0orlem7 16759	Lemma for dichmul0or 16760. (Contributed by Matthew House, 28-Jun-2026.)
|- ( ph -> A. x e. CC A. y e. CC ( ( x x. y ) = 0 -> ( x = 0 \/ y = 0 ) ) )   &    |- ( ph -> A e. RR )   =>    |- ( ph -> ( A <_ 0 \/ 0 <_ A ) )
28-Jun-2026	dichmul0orlem6 16758	Lemma for dichmul0or 16760. (Contributed by Matthew House, 28-Jun-2026.)
|- ( ph -> A e. RR )   &    |- ( ph -> ( ( abs ` A ) - A ) = 0 )   =>    |- ( ph -> 0 <_ A )
28-Jun-2026	msq0 8997	A number is zero iff its square is zero. (Contributed by Matthew House, 28-Jun-2026.)
|- ( A e. CC -> ( ( A x. A ) = 0 <-> A = 0 ) )
28-Jun-2026	msqap0 8996	A number is apart from zero iff its square is apart from zero. (Contributed by Matthew House, 28-Jun-2026.)
|- ( A e. CC -> ( ( A x. A ) # 0 <-> A # 0 ) )
28-Jun-2026	letrid 8442	Tightness of real apartness. (Contributed by Matthew House, 28-Jun-2026.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> B <_ A )   =>    |- ( ph -> A = B )
19-Jun-2026	ringen1zr0 14622	The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). This holds already for nonunital rings, see rngen1zr0 14261, and semirings, see srgen1zr0 14292. (Contributed by FL, 15-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 19-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   &    |- Z = ( 0g ` R )   =>    |- ( ( R e. Ring /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> ( B ~~ 1o <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
19-Jun-2026	srg1zr 14291	The only semiring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 19-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. SRing /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
18-Jun-2026	rngen1zr0 14261	The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 15-Feb-2010.) (Revised by AV, 18-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> ( B ~~ 1o <-> ( .+ = { <. <. .0. , .0. >. , .0. >. } /\ .* = { <. <. .0. , .0. >. , .0. >. } ) ) )
18-Jun-2026	rngen1zr 14260	The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 18-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B ~~ 1o <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
18-Jun-2026	rng1zr 14259	The only ring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 18-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
18-Jun-2026	rng1zrlem 14258	Lemma for rng1zr 14259 and srg1zr 14291. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 18-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. Mgm /\ (mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
17-Jun-2026	ballotfi 13282	Bertrand's ballot problem : the probability that A is ahead throughout the counting. The proof formalized here is a proof "by reflection", as opposed to other known proofs "by induction" or "by permutation". This is Metamath 100 proof #30. (Contributed by Thierry Arnoux, 7-Dec-2016.) (Revised by Jim Kingdon, 17-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   =>    |- ( P ` E ) = ( ( M - N ) / ( M + N ) )
17-Jun-2026	ballotfilembfi 13239	The set of countings where B got the first vote is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- { c e. ( O \ E ) | -. 1 e. c } e. Fin
17-Jun-2026	ballotfilemafi 13238	The set of countings where A got the first vote, but does not stay strictly ahead throughout, is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- { c e. ( O \ E ) | 1 e. c } e. Fin
17-Jun-2026	ballotfilemefi 13237	E is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- E e. Fin
17-Jun-2026	rabxmdc 3554	Law of excluded middle given decidability, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) (Revised by Jim Kingdon, 17-Jun-2026.)
|- ( A. x e. A DECID ph -> A = ( { x e. A | ph } u. { x e. A | -. ph } ) )
15-Jun-2026	ballotfilemgun 13268	A property of the defined .^ operator. (Contributed by Thierry Arnoux, 26-Apr-2017.) (Revised by Jim Kingdon, 15-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. O , v e. Fin |-> ( (♯ ` ( v i^i u ) ) - (♯ ` ( v \ u ) ) ) )   &    |- ( ph -> U e. O )   &    |- ( ph -> L e. ( J ... K ) )   =>    |- ( ph -> ( U .^ ( J ... K ) ) = ( ( U .^ ( J ... ( L - 1 ) ) ) + ( U .^ ( L ... K ) ) ) )
15-Jun-2026	ballotfilemgval 13267	Expand the value of .^. (Contributed by Thierry Arnoux, 21-Apr-2017.) (Revised by Jim Kingdon, 15-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. O , v e. Fin |-> ( (♯ ` ( v i^i u ) ) - (♯ ` ( v \ u ) ) ) )   &    |- ( ph -> U e. O )   &    |- ( ph -> J e. ZZ )   &    |- ( ph -> K e. ZZ )   &    |- ( ph -> V = ( J ... K ) )   =>    |- ( ph -> ( U .^ V ) = ( (♯ ` ( V i^i U ) ) - (♯ ` ( V \ U ) ) ) )
15-Jun-2026	ballotfilemdifcfz 13227	Lemma for ballotfi . The portion of a counting representing votes for B within a specified integer range is finite. (Contributed by Jim Kingdon, 15-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. ZZ )   &    |- ( ph -> K e. ZZ )   =>    |- ( ph -> ( ( J ... K ) \ C ) e. Fin )
15-Jun-2026	ballotfilemcinfz 13226	Lemma for ballotfi . The portion of a counting representing votes for A within a specified integer range is finite. (Contributed by Jim Kingdon, 15-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. ZZ )   &    |- ( ph -> K e. ZZ )   =>    |- ( ph -> ( ( J ... K ) i^i C ) e. Fin )