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 25-Sep-2026 at 6:59 AM ET.

Recent Additions to the Intuitionistic Logic Explorer

Date	Label	Description
Theorem
18-Sep-2026	rirrdisj 17251	The rational and irrational numbers are disjoint. Here irrational means apart from any rational number. (Contributed by Jim Kingdon, 18-Sep-2026.)
|- ( QQ i^i { x e. RR | A. q e. QQ x # q } ) = (/)
16-Sep-2026	cntzm 14155	If the centralizer of a subset of a magma has an element, the magma is inhabited. (Contributed by Jim Kingdon, 16-Sep-2026.)
|- Z = (Cntz ` M )   =>    |- ( X e. ( Z ` S ) -> E. w w e. M )
16-Sep-2026	ressmex 13472	If a structure restriction is inhabited, the structure is a set and so is the class it is restricted to. (Contributed by Jim Kingdon, 16-Sep-2026.)
|- R = ( W ↾s A )   =>    |- ( X e. R -> ( W e. _V /\ A e. _V ) )
15-Sep-2026	cntzex 14144	Set existence of the centralizer. (Contributed by Jim Kingdon, 15-Sep-2026.)
|- Z = (Cntz ` M )   =>    |- ( M e. V -> Z e. _V )
9-Sep-2026	flaplt 10733	The floor function value is less than the next integer. (Contributed by NM, 24-Feb-2005.) (Revised by Jim Kingdon, 9-Sep-2026.)
|- ( ( ( A e. QQ \/ ( A e. RR /\ A. q e. QQ A # q ) ) /\ B e. ZZ ) -> ( A < B <-> ( |_ ` A ) < B ) )
8-Sep-2026	fiidxsupcl 12012	A set of integers indexed by a finite set has an upper bound. (Contributed by Jim Kingdon, 8-Sep-2026.)
|- ( ph -> F : A --> ZZ )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> E. x e. ZZ A. y e. A ( F ` y ) <_ x )
6-Sep-2026	ofrfidc 7318	Decidability of a relation applied to two functions. (Contributed by Jim Kingdon, 6-Sep-2026.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn A )   &    |- ( ph -> A. x e. A DECID ( F ` x ) R ( G ` x ) )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> DECID F oR R G )
27-Aug-2026	prmdcz 12928	Primality is decidable. (Contributed by Jim Kingdon, 27-Aug-2026.)
|- ( N e. ZZ -> DECID N e. Prime )
27-Aug-2026	zmincl 12023	The minumum of two integers is an integer. (Contributed by Jim Kingdon, 27-Aug-2026.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> inf ( { A , B } , RR , < ) e. ZZ )
25-Aug-2026	nn0sqdcq 13007	A nonnegative integer is a perfect square or not. This is similar to nn0sqdc 11162 but expresses the idea of being a perfect square as having a rational number which, when squared, gives the original number. (Contributed by Jim Kingdon, 25-Aug-2026.)
|- ( N e. NN0 -> DECID E. q e. QQ N = ( q ^ 2 ) )
25-Aug-2026	qabscl 11859	The absolute value of a rational number is a rational number. (Contributed by Jim Kingdon, 25-Aug-2026.)
|- ( A e. QQ -> ( abs ` A ) e. QQ )
25-Aug-2026	nn0sqdc 11162	A nonnegative integer is a perfect square or not. (Contributed by Jim Kingdon, 25-Aug-2026.)
|- ( N e. NN0 -> DECID E. q e. NN0 N = ( q ^ 2 ) )
24-Aug-2026	sqrtrirr 13008	The square root of a nonnegative integer is either rational or irrational. (Contributed by Jim Kingdon, 24-Aug-2026.)
|- ( A e. NN0 -> ( ( sqr ` A ) e. QQ \/ ( ( sqr ` A ) e. RR /\ A. q e. QQ ( sqr ` A ) # q ) ) )
21-Aug-2026	prmefexple 16269	Convert a bound on a power of a prime to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Jim Kingdon, 21-Aug-2026.)
|- ( ( A e. Prime /\ N e. ZZ /\ B e. NN ) -> ( ( A ^ N ) <_ B <-> N <_ ( |_ ` ( ( log ` B ) / ( log ` A ) ) ) ) )
20-Aug-2026	zprmlogbap 16179	The logarithm of a natural number to a prime base is either rational or irrational. The proof decomposes X into m e. NN and a e. NN0 such that X = ( ( B ^ a ) x. m ) (using nnmaxpw 12972). If m = 1 the logarithm is a, which is rational. If 1 < m then we can apply logbgcd1irrap 16167 to show that the logarithm is irrational. (Contributed by Jim Kingdon and Taylor Barrella, 20-Aug-2026.)
|- ( ( X e. NN /\ B e. Prime ) -> ( ( B logb X ) e. QQ \/ ( ( B logb X ) e. RR /\ A. q e. QQ ( B logb X ) # q ) ) )
20-Aug-2026	zprmlogbaplem3 16178	Lemma for zprmlogbap 16179. Decomposing a natural number into a power of a prime base and a factor not divisible by that prime. (Contributed by Jim Kingdon, 20-Aug-2026.)
|- J = { z e. NN | -. B || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( B ^ y ) x. x ) )   =>    |- ( ( X e. NN /\ B e. Prime ) -> E. m e. NN E. a e. NN0 ( -. B || m /\ X = ( ( B ^ a ) x. m ) ) )
20-Aug-2026	zprmlogbaplem2 16177	Lemma for zprmlogbap 16179. The logarithm is either rational or irrational. (Contributed by Jim Kingdon, 20-Aug-2026.)
|- ( ph -> B e. Prime )   &    |- ( ph -> M e. NN )   &    |- ( ph -> -. B || M )   &    |- ( ph -> A e. NN0 )   &    |- X = ( ( B ^ A ) x. M )   =>    |- ( ph -> ( ( B logb X ) e. QQ \/ ( ( B logb X ) e. RR /\ A. q e. QQ ( B logb X ) # q ) ) )
20-Aug-2026	zprmlogbaplem1 16176	Lemma for zprmlogbap 16179. Rearranging an expression involving logarithms. (Contributed by Jim Kingdon, 20-Aug-2026.)
|- ( ph -> B e. Prime )   &    |- ( ph -> M e. NN )   &    |- ( ph -> -. B || M )   &    |- ( ph -> A e. NN0 )   =>    |- ( ph -> ( B logb ( ( B ^ A ) x. M ) ) = ( A + ( B logb M ) ) )
20-Aug-2026	flaplelt 10724	A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 20-Aug-2026.)
|- ( ( A e. QQ \/ ( A e. RR /\ A. q e. QQ A # q ) ) -> ( ( |_ ` A ) <_ A /\ A < ( ( |_ ` A ) + 1 ) ) )
20-Aug-2026	flapcl 10722	The floor (greatest integer) function yields an integer when applied to a number which is either rational or irrational. (Contributed by Jim Kingdon, 20-Aug-2026.)
|- ( ( A e. QQ \/ ( A e. RR /\ A. q e. QQ A # q ) ) -> ( |_ ` A ) e. ZZ )
20-Aug-2026	irraddap 10057	The sum of an irrational number and a rational number is irrational. (Contributed by Jim Kingdon, 20-Aug-2026.)
|- ( ( ( A e. RR /\ A. q e. QQ A # q ) /\ B e. QQ ) -> ( ( A + B ) e. RR /\ A. q e. QQ ( A + B ) # q ) )
19-Aug-2026	nnmaxpw 12972	The function F that decomposes a number into its "odd" and "even" parts, which is to say the largest power of a base and largest divisor of the number not divisible by that base, is a bijection from pairs of a nonnegative integer and a number not divisible by that base to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.) (Revised by Jim Kingdon, 19-Aug-2026.)
|- J = { z e. NN | -. B || z }   &    |- F = ( x e. J , y e. NN0 |-> ( ( B ^ y ) x. x ) )   =>    |- ( B e. ( ZZ>= ` 2 ) -> F : ( J X. NN0 ) -1-1-onto-> NN )
19-Aug-2026	nnmaxpwlemparts 12971	Lemma for nnmaxpw 12972. Decomposing a number into parts. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 19-Aug-2026.)
|- ( B e. ( ZZ>= ` 2 ) -> ( ( ( ( X e. NN /\ -. B || X ) /\ Y e. NN0 ) /\ A = ( ( B ^ Y ) x. X ) ) <-> ( A e. NN /\ ( X = ( A / ( B ^ ( iota_ z e. NN0 ( ( B ^ z ) || A /\ -. ( B ^ ( z + 1 ) ) || A ) ) ) ) /\ Y = ( iota_ z e. NN0 ( ( B ^ z ) || A /\ -. ( B ^ ( z + 1 ) ) || A ) ) ) ) ) )
19-Aug-2026	nnmaxpwlemnfac 12970	Lemma for nnmaxpw 12972. Removing the powers of a base from a natural number produces a number not divisible by that base. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 19-Aug-2026.)
|- ( ( A e. NN /\ B e. ( ZZ>= ` 2 ) ) -> -. B || ( A / ( B ^ ( iota_ z e. NN0 ( ( B ^ z ) || A /\ -. ( B ^ ( z + 1 ) ) || A ) ) ) ) )
19-Aug-2026	nnmaxpwlemndvds 12969	Lemma for nnmaxpw 12972. A natural number is not divisible by one more than the highest power of a base which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.) (Revised by Jim Kingdon, 19-Aug-2026.)
|- ( ( A e. NN /\ B e. ( ZZ>= ` 2 ) ) -> -. ( B ^ ( ( iota_ z e. NN0 ( ( B ^ z ) || A /\ -. ( B ^ ( z + 1 ) ) || A ) ) + 1 ) ) || A )
19-Aug-2026	nnmaxpwlemdvds 12968	Lemma for nnmaxpw 12972. A natural number is divisible by the highest power of a base which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.) (Revised by Jim Kingdon, 19-Aug-2026.)
|- ( ( A e. NN /\ B e. ( ZZ>= ` 2 ) ) -> ( B ^ ( iota_ z e. NN0 ( ( B ^ z ) || A /\ -. ( B ^ ( z + 1 ) ) || A ) ) ) || A )
18-Aug-2026	nnmaxpwlemxy 12967	Lemma for nnmaxpw 12972. Another way of stating that decomposing a natural number into a power of a base and a number not divisible by that base is unique. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 18-Aug-2026.)
|- ( ph -> X e. NN )   &    |- ( ph -> B e. ( ZZ>= ` 2 ) )   &    |- ( ph -> -. B || X )   &    |- ( ph -> Y e. NN0 )   &    |- ( ph -> A = ( ( B ^ Y ) x. X ) )   =>    |- ( ph -> ( X = ( A / ( B ^ ( iota_ z e. NN0 ( ( B ^ z ) || A /\ -. ( B ^ ( z + 1 ) ) || A ) ) ) ) /\ Y = ( iota_ z e. NN0 ( ( B ^ z ) || A /\ -. ( B ^ ( z + 1 ) ) || A ) ) ) )
18-Aug-2026	pwbdvdseu 12966	A natural number has a unique highest power of a base which divides it. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 18-Aug-2026.)
|- ( ( N e. NN /\ B e. ( ZZ>= ` 2 ) ) -> E! m e. NN0 ( ( B ^ m ) || N /\ -. ( B ^ ( m + 1 ) ) || N ) )
18-Aug-2026	pwbdvdseulemle 12965	Lemma for pwbdvdseu 12966. Powers of a base which do and do not divide a natural number. (Contributed by Jim Kingdon, 17-Nov-2021.) (Revised by Jim Kingdon, 18-Aug-2026.)
|- ( ph -> N e. NN )   &    |- ( ph -> A e. NN0 )   &    |- ( ph -> B e. NN0 )   &    |- ( ph -> P e. NN )   &    |- ( ph -> ( P ^ A ) || N )   &    |- ( ph -> -. ( P ^ ( B + 1 ) ) || N )   =>    |- ( ph -> A <_ B )
18-Aug-2026	pwbdvds 12964	A natural number has a highest power of a base which divides it. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 18-Aug-2026.)
|- ( ( N e. NN /\ B e. ( ZZ>= ` 2 ) ) -> E. m e. NN0 ( ( B ^ m ) || N /\ -. ( B ^ ( m + 1 ) ) || N ) )
17-Aug-2026	pwbdvdslemn 12963	Lemma for pwbdvds 12964. If a natural number has some power of a base which does not divide it, there is a highest power of the base which does divide it. (Contributed by Jim Kingdon, 14-Nov-2021.) (Revised by Jim Kingdon, 17-Aug-2026.)
|- ( ph -> N e. NN )   &    |- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> -. ( B ^ A ) || N )   =>    |- ( ph -> E. m e. NN0 ( ( B ^ m ) || N /\ -. ( B ^ ( m + 1 ) ) || N ) )
14-Aug-2026	reaplog 16061	Apartness and the real natural logarithm. (Contributed by Jim Kingdon, 14-Aug-2026.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A # B <-> ( log ` A ) # ( log ` B ) ) )
13-Aug-2026	efap1p 15971	If the exponential of a number is apart from one plus that number, the number is apart from zero. To some extent can be thought of as the converse of efgt1p 12482. (Contributed by Jim Kingdon, 13-Aug-2026.)
|- ( ( A e. RR /\ ( 1 + A ) # ( exp ` A ) ) -> A # 0 )
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 17212	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 17211	Lemma for wexmiddifxylem 17211. 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 17200	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 17208	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 17207	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 17210	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 17209	Lemma for wexmiddiffi 17210. 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 ) )
28-Jul-2026	psrbaglefifi 15147	There are finitely many bags dominated by a given bag. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 25-Jan-2015.) (Revised by Jim Kingdon, 28-Jul-2026.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( F e. D /\ I e. Fin ) -> { y e. D | y oR <_ F } e. Fin )
24-Jul-2026	stnot 17205	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 13467	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 17346	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 17314 by alseuals 17332. See als-no-surprise 17314 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 17345	"The ph is ps " implies that exactly one thing is both ph and ps. This is the half of dfalseu2 17344 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 17344	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 17329 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 17345 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 17343	Bound-variable hypothesis builder for "all some one" restricted to a class. This is the "all some one" counterpart of nfrals 17312. (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 17342	Bound-variable hypothesis builder for "all some one". This is the "all some one" counterpart of nfals 17311. 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 17341	Congruence for "all some one" restricted to a class. This is the "all some one" counterpart of ralsbii 17309. (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 17340	Congruence: equivalents may be substituted inside an "all some one". This is the "all some one" counterpart of alsbii 17308. (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 17339	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 17338	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 17337	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 17336	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 17335	Introduction rule for "all some one" restricted to a class. This is the converse of ralseu1d 17338 and ralseu2d 17339 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 17334	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 17336 and alseu2d 17337 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 17333	"All some one" restricted to a class implies "all some" restricted to that class. Restricted counterpart of alseuals 17332. (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 17332	"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 17346 is proved. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x ( ph -> ps ) -> A.E. x ( ph -> ps ) )
22-Jul-2026	dfralseu2 17331	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 17297. (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 17330	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 17329	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 17328	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 17327	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 17326	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 17325	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 17324	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 17321	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 17320	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 17319	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 17318. (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 17318	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 17317	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 17323. (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 17316	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 17322. (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 17314	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 17295: 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 17305	Deduction rule: Given "all some" applied to a class, the class is inhabited. This is stronger than ralsn0d 17304, 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 17323	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 17317 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 17322	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 17316 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 17315	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 17314, and follows from it by dfrals2 17297. 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 17313	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 17312	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 17311	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 17310	Deduction form of alsbii 17308. (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 17309	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 17308	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 17307	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 17306. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( A.E. x e. A ( ph -> ps ) -> E. x e. A ps )
12-Jul-2026	alsex 17306	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 17314, 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 17304	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 17303	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 17302	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 17299	Introduction rule for "all some" restricted to a class. This is the converse of rals1d 17302 and rals2d 17303 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 17298	Introduction rule: "all some" holds if the "for all" part holds and the antecedent has a witness. This is the converse of als1d 17300 and als2d 17301 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 ) )