Theorem axsepg5

Description: A generalization of ax-sep that combines axsepg , axsepg2 , and axsepg3 into a single theorem scheme. Unlike ax-sep , this scheme lacks a distinct variable condition for ph and z , for x and z , and for y and z . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BTernaryTau, 24-May-2026) (New usage is discouraged.)

	Ref	Expression
Assertion	axsepg5	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		nfnae	|- F/ x -. A. y y = z
2		nfvd	|- ( -. A. y y = z -> F/ y x e. w )
3		nfcvf	|- ( -. A. y y = z -> F/_ y z )
4	3	nfcrd	|- ( -. A. y y = z -> F/ y x e. z )
5		nfvd	|- ( -. A. y y = z -> F/ y ph )
6	4 5	nfand	|- ( -. A. y y = z -> F/ y ( x e. z /\ ph ) )
7	2 6	nfbid	|- ( -. A. y y = z -> F/ y ( x e. w <-> ( x e. z /\ ph ) ) )
8	1 7	nfald	|- ( -. A. y y = z -> F/ y A. x ( x e. w <-> ( x e. z /\ ph ) ) )
9		nfvd	|- ( -. A. y y = z -> F/ w A. x ( x e. y <-> ( x e. z /\ ph ) ) )
10		elequ2	|- ( w = y -> ( x e. w <-> x e. y ) )
11	10	bibi1d	|- ( w = y -> ( ( x e. w <-> ( x e. z /\ ph ) ) <-> ( x e. y <-> ( x e. z /\ ph ) ) ) )
12	11	albidv	|- ( w = y -> ( A. x ( x e. w <-> ( x e. z /\ ph ) ) <-> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
13	12	biimpd	|- ( w = y -> ( A. x ( x e. w <-> ( x e. z /\ ph ) ) -> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
14	13	a1i	|- ( -. A. y y = z -> ( w = y -> ( A. x ( x e. w <-> ( x e. z /\ ph ) ) -> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) ) )
15		nfae	|- F/ x A. y y = z
16		elequ2	|- ( y = z -> ( x e. y <-> x e. z ) )
17	16	anbi1d	|- ( y = z -> ( ( x e. y /\ ph ) <-> ( x e. z /\ ph ) ) )
18	17	bibi2d	|- ( y = z -> ( ( x e. y <-> ( x e. y /\ ph ) ) <-> ( x e. y <-> ( x e. z /\ ph ) ) ) )
19	18	biimpd	|- ( y = z -> ( ( x e. y <-> ( x e. y /\ ph ) ) -> ( x e. y <-> ( x e. z /\ ph ) ) ) )
20	19	sps	|- ( A. y y = z -> ( ( x e. y <-> ( x e. y /\ ph ) ) -> ( x e. y <-> ( x e. z /\ ph ) ) ) )
21	15 20	alimd	|- ( A. y y = z -> ( A. x ( x e. y <-> ( x e. y /\ ph ) ) -> A. x ( x e. y <-> ( x e. z /\ ph ) ) ) )
22		axsepg4	|- E. w A. x ( x e. w <-> ( x e. z /\ ph ) )
23		axsepg3	|- E. y A. x ( x e. y <-> ( x e. y /\ ph ) )
24	8 9 14 21 22 23	dvelimexcasei	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )