Theorem sn-axrep5v

Description: A condensed form of axrep5 . (Contributed by SN, 21-Sep-2023)

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

Proof

Step	Hyp	Ref	Expression
1		axrep6	|- ( A. w E* z ( w e. x /\ ph ) -> E. y A. z ( z e. y <-> E. w e. x ( w e. x /\ ph ) ) )
2		19.37v	|- ( E. y ( w e. x -> A. z ( ph -> z = y ) ) <-> ( w e. x -> E. y A. z ( ph -> z = y ) ) )
3		impexp	|- ( ( ( w e. x /\ ph ) -> z = y ) <-> ( w e. x -> ( ph -> z = y ) ) )
4	3	albii	|- ( A. z ( ( w e. x /\ ph ) -> z = y ) <-> A. z ( w e. x -> ( ph -> z = y ) ) )
5		19.21v	|- ( A. z ( w e. x -> ( ph -> z = y ) ) <-> ( w e. x -> A. z ( ph -> z = y ) ) )
6	4 5	bitri	|- ( A. z ( ( w e. x /\ ph ) -> z = y ) <-> ( w e. x -> A. z ( ph -> z = y ) ) )
7	6	exbii	|- ( E. y A. z ( ( w e. x /\ ph ) -> z = y ) <-> E. y ( w e. x -> A. z ( ph -> z = y ) ) )
8		df-mo	|- ( E* z ph <-> E. y A. z ( ph -> z = y ) )
9	8	imbi2i	|- ( ( w e. x -> E* z ph ) <-> ( w e. x -> E. y A. z ( ph -> z = y ) ) )
10	2 7 9	3bitr4i	|- ( E. y A. z ( ( w e. x /\ ph ) -> z = y ) <-> ( w e. x -> E* z ph ) )
11	10	albii	|- ( A. w E. y A. z ( ( w e. x /\ ph ) -> z = y ) <-> A. w ( w e. x -> E* z ph ) )
12		df-mo	|- ( E* z ( w e. x /\ ph ) <-> E. y A. z ( ( w e. x /\ ph ) -> z = y ) )
13	12	albii	|- ( A. w E* z ( w e. x /\ ph ) <-> A. w E. y A. z ( ( w e. x /\ ph ) -> z = y ) )
14		df-ral	|- ( A. w e. x E* z ph <-> A. w ( w e. x -> E* z ph ) )
15	11 13 14	3bitr4i	|- ( A. w E* z ( w e. x /\ ph ) <-> A. w e. x E* z ph )
16		rexanid	|- ( E. w e. x ( w e. x /\ ph ) <-> E. w e. x ph )
17	16	bibi2i	|- ( ( z e. y <-> E. w e. x ( w e. x /\ ph ) ) <-> ( z e. y <-> E. w e. x ph ) )
18	17	albii	|- ( A. z ( z e. y <-> E. w e. x ( w e. x /\ ph ) ) <-> A. z ( z e. y <-> E. w e. x ph ) )
19	18	exbii	|- ( E. y A. z ( z e. y <-> E. w e. x ( w e. x /\ ph ) ) <-> E. y A. z ( z e. y <-> E. w e. x ph ) )
20	1 15 19	3imtr3i	|- ( A. w e. x E* z ph -> E. y A. z ( z e. y <-> E. w e. x ph ) )