Theorem ac6s6f

Description: Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 20-Aug-2018)

	Ref	Expression
Hypotheses	ac6s6f.1	|- A e. _V
	ac6s6f.2	|- F/ y ps
	ac6s6f.3	|- ( y = ( f ` x ) -> ( ph <-> ps ) )
	ac6s6f.4	|- F/_ x A
Assertion	ac6s6f	|- E. f A. x e. A ( E. y ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		ac6s6f.1	|- A e. _V
2		ac6s6f.2	|- F/ y ps
3		ac6s6f.3	|- ( y = ( f ` x ) -> ( ph <-> ps ) )
4		ac6s6f.4	|- F/_ x A
5	1	isseti	|- E. z z = A
6		vex	|- z e. _V
7	2 6 3	ac6s6	|- E. f A. x e. z ( E. y ph -> ps )
8	5 7	exan	|- E. z ( z = A /\ E. f A. x e. z ( E. y ph -> ps ) )
9		exdistr	|- ( E. z E. f ( z = A /\ A. x e. z ( E. y ph -> ps ) ) <-> E. z ( z = A /\ E. f A. x e. z ( E. y ph -> ps ) ) )
10	8 9	mpbir	|- E. z E. f ( z = A /\ A. x e. z ( E. y ph -> ps ) )
11		nfcv	|- F/_ x z
12	11 4	raleqf	|- ( z = A -> ( A. x e. z ( E. y ph -> ps ) <-> A. x e. A ( E. y ph -> ps ) ) )
13	12	biimpa	|- ( ( z = A /\ A. x e. z ( E. y ph -> ps ) ) -> A. x e. A ( E. y ph -> ps ) )
14	13	2eximi	|- ( E. z E. f ( z = A /\ A. x e. z ( E. y ph -> ps ) ) -> E. z E. f A. x e. A ( E. y ph -> ps ) )
15		ax5e	|- ( E. z E. f A. x e. A ( E. y ph -> ps ) -> E. f A. x e. A ( E. y ph -> ps ) )
16	10 14 15	mp2b	|- E. f A. x e. A ( E. y ph -> ps )