Theorem axrep6

Description: A condensed form of ax-rep . (Contributed by SN, 18-Sep-2023)

	Ref	Expression
Assertion	axrep6	|- ( A. w E* z ph -> E. y A. z ( z e. y <-> E. w e. x ph ) )

Proof

Step	Hyp	Ref	Expression
1		ax-rep	|- ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
2		df-mo	|- ( E* z ph <-> E. y A. z ( ph -> z = y ) )
3		19.3v	|- ( A. y ph <-> ph )
4	3	imbi1i	|- ( ( A. y ph -> z = y ) <-> ( ph -> z = y ) )
5	4	albii	|- ( A. z ( A. y ph -> z = y ) <-> A. z ( ph -> z = y ) )
6	5	exbii	|- ( E. y A. z ( A. y ph -> z = y ) <-> E. y A. z ( ph -> z = y ) )
7	2 6	bitr4i	|- ( E* z ph <-> E. y A. z ( A. y ph -> z = y ) )
8	7	albii	|- ( A. w E* z ph <-> A. w E. y A. z ( A. y ph -> z = y ) )
9	3	rexbii	|- ( E. w e. x A. y ph <-> E. w e. x ph )
10		df-rex	|- ( E. w e. x A. y ph <-> E. w ( w e. x /\ A. y ph ) )
11	9 10	bitr3i	|- ( E. w e. x ph <-> E. w ( w e. x /\ A. y ph ) )
12	11	bibi2i	|- ( ( z e. y <-> E. w e. x ph ) <-> ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
13	12	albii	|- ( A. z ( z e. y <-> E. w e. x ph ) <-> A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
14	13	exbii	|- ( E. y A. z ( z e. y <-> E. w e. x ph ) <-> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
15	1 8 14	3imtr4i	|- ( A. w E* z ph -> E. y A. z ( z e. y <-> E. w e. x ph ) )