Theorem bj-rep

Description: Version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function from ax-rep (in the form of axrep6 ). (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.) (New usage is discouraded.)

	Ref	Expression
Assertion	bj-rep	|- A. x ( A. y e. x E! z ph -> E. t A. z ( z e. t <-> E. y e. x ph ) )

Proof

Step	Hyp	Ref	Expression
1		df-ral	|- ( A. y e. x E! z ph <-> A. y ( y e. x -> E! z ph ) )
2		eumo	|- ( E! z ph -> E* z ph )
3	2	imim2i	|- ( ( y e. x -> E! z ph ) -> ( y e. x -> E* z ph ) )
4		moanimv	|- ( E* z ( y e. x /\ ph ) <-> ( y e. x -> E* z ph ) )
5	3 4	sylibr	|- ( ( y e. x -> E! z ph ) -> E* z ( y e. x /\ ph ) )
6	5	alimi	|- ( A. y ( y e. x -> E! z ph ) -> A. y E* z ( y e. x /\ ph ) )
7	1 6	sylbi	|- ( A. y e. x E! z ph -> A. y E* z ( y e. x /\ ph ) )
8		axrep6	|- ( A. y E* z ( y e. x /\ ph ) -> E. t A. z ( z e. t <-> E. y e. x ( y e. x /\ ph ) ) )
9		rexanid	|- ( E. y e. x ( y e. x /\ ph ) <-> E. y e. x ph )
10	9	bibi2i	|- ( ( z e. t <-> E. y e. x ( y e. x /\ ph ) ) <-> ( z e. t <-> E. y e. x ph ) )
11	10	albii	|- ( A. z ( z e. t <-> E. y e. x ( y e. x /\ ph ) ) <-> A. z ( z e. t <-> E. y e. x ph ) )
12	11	exbii	|- ( E. t A. z ( z e. t <-> E. y e. x ( y e. x /\ ph ) ) <-> E. t A. z ( z e. t <-> E. y e. x ph ) )
13	8 12	sylib	|- ( A. y E* z ( y e. x /\ ph ) -> E. t A. z ( z e. t <-> E. y e. x ph ) )
14	7 13	syl	|- ( A. y e. x E! z ph -> E. t A. z ( z e. t <-> E. y e. x ph ) )
15	14	ax-gen	|- A. x ( A. y e. x E! z ph -> E. t A. z ( z e. t <-> E. y e. x ph ) )