Theorem bj-axseprep

Description: Axiom of separation (universal closure of ax-sep ) from a weak form of the axiom of replacement requiring that the functional relation in it be a (total) function and the weak emptyset axiom (existence of an empty set provided existence of a set), as written in the theorem's hypotheses.

This result shows that the weak emptyset axiom is not only the result of a cheap way to avoid an axiom redundancy (in this case, the existence axiom extru ) by adding it as an antecedent, but also permits to prove nontrivial results that hold in nonnecessarily nonempty universes.

This proof is by cases so is not intuitionistic. The statement does not require a nonempty universe; most of the proof does not either, and the parts that do (e.g., near sb8ef and sbequ12r and eueq2 ) could be reworked to avoid it. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv . (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-axseprep.axnulw	|- ( E. x T. -> E. y A. z e. y F. )
	bj-axseprep.axrep	|- A. x ( A. z e. x E! t ps -> E. y A. t ( t e. y <-> E. z e. x ps ) )
	bj-axseprep.ps	|- ( ps <-> ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) )
Assertion	bj-axseprep	|- A. x E. y A. z ( z e. y <-> ( z e. x /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		bj-axseprep.axnulw	|- ( E. x T. -> E. y A. z e. y F. )
2		bj-axseprep.axrep	|- A. x ( A. z e. x E! t ps -> E. y A. t ( t e. y <-> E. z e. x ps ) )
3		bj-axseprep.ps	|- ( ps <-> ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) )
4		ax5e	|- ( E. a E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) )
5	4	ax-gen	|- A. x ( E. a E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) )
6		bj-eximcom	|- ( E. a ( E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) ) -> ( A. a E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) -> E. a E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) ) )
7	3	eubii	|- ( E! t ps <-> E! t ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) )
8	7	ralbii	|- ( A. z e. x E! t ps <-> A. z e. x E! t ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) )
9	3	rexbii	|- ( E. z e. x ps <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) )
10	9	bibi2i	|- ( ( t e. y <-> E. z e. x ps ) <-> ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) )
11	10	albii	|- ( A. t ( t e. y <-> E. z e. x ps ) <-> A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) )
12	11	exbii	|- ( E. y A. t ( t e. y <-> E. z e. x ps ) <-> E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) )
13	8 12	imbi12i	|- ( ( A. z e. x E! t ps -> E. y A. t ( t e. y <-> E. z e. x ps ) ) <-> ( A. z e. x E! t ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) -> E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) ) )
14	13	albii	|- ( A. x ( A. z e. x E! t ps -> E. y A. t ( t e. y <-> E. z e. x ps ) ) <-> A. x ( A. z e. x E! t ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) -> E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) ) )
15	2 14	mpbi	|- A. x ( A. z e. x E! t ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) -> E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) )
16		vex	|- z e. _V
17		vex	|- a e. _V
18	16 17	eueq2	|- E! t ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) )
19	18	rgenw	|- A. z e. x E! t ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) )
20	19	ax-gen	|- A. x A. z e. x E! t ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) )
21	15 20	bj-almp	|- A. x E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) )
22	21	ax-gen	|- A. a A. x E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) )
23		alcom	|- ( A. a A. x E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) <-> A. x A. a E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) )
24	22 23	mpbi	|- A. x A. a E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) )
25	6 24	bj-almpig	|- A. x ( E. a ( E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) ) -> E. a E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) )
26		df-rex	|- ( E. z e. x ph <-> E. z ( z e. x /\ ph ) )
27		nfv	|- F/ a ( z e. x /\ ph )
28	27	sb8ef	|- ( E. z ( z e. x /\ ph ) <-> E. a [ a / z ] ( z e. x /\ ph ) )
29	26 28	bitri	|- ( E. z e. x ph <-> E. a [ a / z ] ( z e. x /\ ph ) )
30		df-rex	|- ( E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) <-> E. z ( z e. x /\ ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) )
31		andi	|- ( ( z e. x /\ ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) <-> ( ( z e. x /\ ( ph /\ t = z ) ) \/ ( z e. x /\ ( -. ph /\ t = a ) ) ) )
32	31	exbii	|- ( E. z ( z e. x /\ ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) <-> E. z ( ( z e. x /\ ( ph /\ t = z ) ) \/ ( z e. x /\ ( -. ph /\ t = a ) ) ) )
33		19.43	|- ( E. z ( ( z e. x /\ ( ph /\ t = z ) ) \/ ( z e. x /\ ( -. ph /\ t = a ) ) ) <-> ( E. z ( z e. x /\ ( ph /\ t = z ) ) \/ E. z ( z e. x /\ ( -. ph /\ t = a ) ) ) )
34	30 32 33	3bitri	|- ( E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) <-> ( E. z ( z e. x /\ ( ph /\ t = z ) ) \/ E. z ( z e. x /\ ( -. ph /\ t = a ) ) ) )
35		equcom	|- ( z = t <-> t = z )
36	35	anbi1i	|- ( ( z = t /\ ( z e. x /\ ph ) ) <-> ( t = z /\ ( z e. x /\ ph ) ) )
37		ancom	|- ( ( t = z /\ ( z e. x /\ ph ) ) <-> ( ( z e. x /\ ph ) /\ t = z ) )
38		anass	|- ( ( ( z e. x /\ ph ) /\ t = z ) <-> ( z e. x /\ ( ph /\ t = z ) ) )
39	36 37 38	3bitri	|- ( ( z = t /\ ( z e. x /\ ph ) ) <-> ( z e. x /\ ( ph /\ t = z ) ) )
40	39	exbii	|- ( E. z ( z = t /\ ( z e. x /\ ph ) ) <-> E. z ( z e. x /\ ( ph /\ t = z ) ) )
41	40	biimpri	|- ( E. z ( z e. x /\ ( ph /\ t = z ) ) -> E. z ( z = t /\ ( z e. x /\ ph ) ) )
42	41	a1i	|- ( [ a / z ] ( z e. x /\ ph ) -> ( E. z ( z e. x /\ ( ph /\ t = z ) ) -> E. z ( z = t /\ ( z e. x /\ ph ) ) ) )
43		simprr	|- ( ( z e. x /\ ( -. ph /\ t = a ) ) -> t = a )
44	43	exlimiv	|- ( E. z ( z e. x /\ ( -. ph /\ t = a ) ) -> t = a )
45		sbequi	|- ( a = t -> ( [ a / z ] ( z e. x /\ ph ) -> [ t / z ] ( z e. x /\ ph ) ) )
46	45	equcoms	|- ( t = a -> ( [ a / z ] ( z e. x /\ ph ) -> [ t / z ] ( z e. x /\ ph ) ) )
47	46	com12	|- ( [ a / z ] ( z e. x /\ ph ) -> ( t = a -> [ t / z ] ( z e. x /\ ph ) ) )
48		sb5	|- ( [ t / z ] ( z e. x /\ ph ) <-> E. z ( z = t /\ ( z e. x /\ ph ) ) )
49	47 48	imbitrdi	|- ( [ a / z ] ( z e. x /\ ph ) -> ( t = a -> E. z ( z = t /\ ( z e. x /\ ph ) ) ) )
50	44 49	syl5	|- ( [ a / z ] ( z e. x /\ ph ) -> ( E. z ( z e. x /\ ( -. ph /\ t = a ) ) -> E. z ( z = t /\ ( z e. x /\ ph ) ) ) )
51	42 50	jaod	|- ( [ a / z ] ( z e. x /\ ph ) -> ( ( E. z ( z e. x /\ ( ph /\ t = z ) ) \/ E. z ( z e. x /\ ( -. ph /\ t = a ) ) ) -> E. z ( z = t /\ ( z e. x /\ ph ) ) ) )
52		orc	|- ( E. z ( z e. x /\ ( ph /\ t = z ) ) -> ( E. z ( z e. x /\ ( ph /\ t = z ) ) \/ E. z ( z e. x /\ ( -. ph /\ t = a ) ) ) )
53	40 52	sylbi	|- ( E. z ( z = t /\ ( z e. x /\ ph ) ) -> ( E. z ( z e. x /\ ( ph /\ t = z ) ) \/ E. z ( z e. x /\ ( -. ph /\ t = a ) ) ) )
54	51 53	impbid1	|- ( [ a / z ] ( z e. x /\ ph ) -> ( ( E. z ( z e. x /\ ( ph /\ t = z ) ) \/ E. z ( z e. x /\ ( -. ph /\ t = a ) ) ) <-> E. z ( z = t /\ ( z e. x /\ ph ) ) ) )
55	34 54	bitrid	|- ( [ a / z ] ( z e. x /\ ph ) -> ( E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) <-> E. z ( z = t /\ ( z e. x /\ ph ) ) ) )
56	55	bibi2d	|- ( [ a / z ] ( z e. x /\ ph ) -> ( ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) <-> ( t e. y <-> E. z ( z = t /\ ( z e. x /\ ph ) ) ) ) )
57	56	biimpd	|- ( [ a / z ] ( z e. x /\ ph ) -> ( ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) -> ( t e. y <-> E. z ( z = t /\ ( z e. x /\ ph ) ) ) ) )
58	57	alimdv	|- ( [ a / z ] ( z e. x /\ ph ) -> ( A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) -> A. t ( t e. y <-> E. z ( z = t /\ ( z e. x /\ ph ) ) ) ) )
59		nfv	|- F/ z t e. y
60		nfe1	|- F/ z E. z ( z = t /\ ( z e. x /\ ph ) )
61	59 60	nfbi	|- F/ z ( t e. y <-> E. z ( z = t /\ ( z e. x /\ ph ) ) )
62		nfv	|- F/ t ( z e. y <-> ( z e. x /\ ph ) )
63		elequ1	|- ( t = z -> ( t e. y <-> z e. y ) )
64	48	bicomi	|- ( E. z ( z = t /\ ( z e. x /\ ph ) ) <-> [ t / z ] ( z e. x /\ ph ) )
65		sbequ12r	|- ( t = z -> ( [ t / z ] ( z e. x /\ ph ) <-> ( z e. x /\ ph ) ) )
66	64 65	bitrid	|- ( t = z -> ( E. z ( z = t /\ ( z e. x /\ ph ) ) <-> ( z e. x /\ ph ) ) )
67	63 66	bibi12d	|- ( t = z -> ( ( t e. y <-> E. z ( z = t /\ ( z e. x /\ ph ) ) ) <-> ( z e. y <-> ( z e. x /\ ph ) ) ) )
68	61 62 67	cbvalv1	|- ( A. t ( t e. y <-> E. z ( z = t /\ ( z e. x /\ ph ) ) ) <-> A. z ( z e. y <-> ( z e. x /\ ph ) ) )
69	58 68	imbitrdi	|- ( [ a / z ] ( z e. x /\ ph ) -> ( A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) -> A. z ( z e. y <-> ( z e. x /\ ph ) ) ) )
70	69	eximdv	|- ( [ a / z ] ( z e. x /\ ph ) -> ( E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) ) )
71	70	eximi	|- ( E. a [ a / z ] ( z e. x /\ ph ) -> E. a ( E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) ) )
72	29 71	sylbi	|- ( E. z e. x ph -> E. a ( E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) ) )
73	72	ax-gen	|- A. x ( E. z e. x ph -> E. a ( E. y A. t ( t e. y <-> E. z e. x ( ( ph /\ t = z ) \/ ( -. ph /\ t = a ) ) ) -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) ) )
74	25 73	barbara	|- A. x ( E. z e. x ph -> E. a E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) )
75	5 74	barbara	|- A. x ( E. z e. x ph -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) )
76		ralnex	|- ( A. z e. x -. ph <-> -. E. z e. x ph )
77		df-ral	|- ( A. z e. x -. ph <-> A. z ( z e. x -> -. ph ) )
78		df-ral	|- ( A. z e. y F. <-> A. z ( z e. y -> F. ) )
79		dfnot	|- ( -. z e. y <-> ( z e. y -> F. ) )
80	79	bicomi	|- ( ( z e. y -> F. ) <-> -. z e. y )
81		imnan	|- ( ( z e. x -> -. ph ) <-> -. ( z e. x /\ ph ) )
82		pm5.21	|- ( ( -. z e. y /\ -. ( z e. x /\ ph ) ) -> ( z e. y <-> ( z e. x /\ ph ) ) )
83	80 81 82	syl2anb	|- ( ( ( z e. y -> F. ) /\ ( z e. x -> -. ph ) ) -> ( z e. y <-> ( z e. x /\ ph ) ) )
84	83	expcom	|- ( ( z e. x -> -. ph ) -> ( ( z e. y -> F. ) -> ( z e. y <-> ( z e. x /\ ph ) ) ) )
85	84	al2imi	|- ( A. z ( z e. x -> -. ph ) -> ( A. z ( z e. y -> F. ) -> A. z ( z e. y <-> ( z e. x /\ ph ) ) ) )
86	78 85	biimtrid	|- ( A. z ( z e. x -> -. ph ) -> ( A. z e. y F. -> A. z ( z e. y <-> ( z e. x /\ ph ) ) ) )
87	77 86	sylbi	|- ( A. z e. x -. ph -> ( A. z e. y F. -> A. z ( z e. y <-> ( z e. x /\ ph ) ) ) )
88	76 87	sylbir	|- ( -. E. z e. x ph -> ( A. z e. y F. -> A. z ( z e. y <-> ( z e. x /\ ph ) ) ) )
89	88	eximdv	|- ( -. E. z e. x ph -> ( E. y A. z e. y F. -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) ) )
90		bj-alextruim	|- ( A. x E. y A. z e. y F. <-> ( E. x T. -> E. y A. z e. y F. ) )
91	1 90	mpbir	|- A. x E. y A. z e. y F.
92	89 91	bj-almpig	|- A. x ( -. E. z e. x ph -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) )
93		pm2.61	|- ( ( E. z e. x ph -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) ) -> ( ( -. E. z e. x ph -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) ) -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) ) )
94	93	al2imi	|- ( A. x ( E. z e. x ph -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) ) -> ( A. x ( -. E. z e. x ph -> E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) ) -> A. x E. y A. z ( z e. y <-> ( z e. x /\ ph ) ) ) )
95	75 92 94	mp2	|- A. x E. y A. z ( z e. y <-> ( z e. x /\ ph ) )