Theorem axsepgfromrep

Description: A more general version axsepg of the axiom scheme of separation ax-sep derived from the axiom scheme of replacement ax-rep (and first-order logic). The extra generality consists in the absence of a disjoint variable condition on z , ph (that is, variable z may occur in formula ph ). See linked statements for more information. (Contributed by NM, 11-Sep-2006) Remove dependencies on ax-9 to ax-13 . (Revised by SN, 25-Sep-2023) Use ax-sep instead (or axsepg if the extra generality is needed). (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		axrep6	|- ( A. w E* x ( w = x /\ ph ) -> E. y A. x ( x e. y <-> E. w e. z ( w = x /\ ph ) ) )
2		euequ	|- E! x x = w
3	2	eumoi	|- E* x x = w
4		equcomi	|- ( w = x -> x = w )
5	4	adantr	|- ( ( w = x /\ ph ) -> x = w )
6	5	moimi	|- ( E* x x = w -> E* x ( w = x /\ ph ) )
7	3 6	ax-mp	|- E* x ( w = x /\ ph )
8	1 7	mpg	|- E. y A. x ( x e. y <-> E. w e. z ( w = x /\ ph ) )
9		df-rex	|- ( E. w e. z ( w = x /\ ph ) <-> E. w ( w e. z /\ ( w = x /\ ph ) ) )
10		an12	|- ( ( w = x /\ ( w e. z /\ ph ) ) <-> ( w e. z /\ ( w = x /\ ph ) ) )
11	10	exbii	|- ( E. w ( w = x /\ ( w e. z /\ ph ) ) <-> E. w ( w e. z /\ ( w = x /\ ph ) ) )
12		elequ1	|- ( w = x -> ( w e. z <-> x e. z ) )
13	12	anbi1d	|- ( w = x -> ( ( w e. z /\ ph ) <-> ( x e. z /\ ph ) ) )
14	13	equsexvw	|- ( E. w ( w = x /\ ( w e. z /\ ph ) ) <-> ( x e. z /\ ph ) )
15	9 11 14	3bitr2i	|- ( E. w e. z ( w = x /\ ph ) <-> ( x e. z /\ ph ) )
16	15	bibi2i	|- ( ( x e. y <-> E. w e. z ( w = x /\ ph ) ) <-> ( x e. y <-> ( x e. z /\ ph ) ) )
17	16	albii	|- ( A. x ( x e. y <-> E. w e. z ( w = x /\ ph ) ) <-> A. x ( x e. y <-> ( x e. z /\ ph ) ) )
18	17	exbii	|- ( E. y A. x ( x e. y <-> E. w e. z ( w = x /\ ph ) ) <-> E. y A. x ( x e. y <-> ( x e. z /\ ph ) ) )
19	8 18	mpbi	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )