Theorem ac6num

Description: A version of ac6 which takes the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypothesis	ac6num.1	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ac6num	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ac6num.1	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		nfiu1	$$⊢\underset{\_}{Ⅎ}x\bigcup _{x\in A}\left\{y\in B|\phi \right\}$$
3	2	nfel1	$$⊢Ⅎx\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}$$
4		ssiun2	$$⊢x\in A\to \left\{y\in B|\phi \right\}\subseteq \bigcup _{x\in A}\left\{y\in B|\phi \right\}$$
5		ssexg	$$⊢\left(\left\{y\in B|\phi \right\}\subseteq \bigcup _{x\in A}\left\{y\in B|\phi \right\}\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\right)\to \left\{y\in B|\phi \right\}\in \mathrm{V}$$
6	5	expcom	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\to \left(\left\{y\in B|\phi \right\}\subseteq \bigcup _{x\in A}\left\{y\in B|\phi \right\}\to \left\{y\in B|\phi \right\}\in \mathrm{V}\right)$$
7	4 6	syl5	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\to \left(x\in A\to \left\{y\in B|\phi \right\}\in \mathrm{V}\right)$$
8	3 7	ralrimi	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\to \forall x\in A\left\{y\in B|\phi \right\}\in \mathrm{V}$$
9		dfiun2g	$$⊢\forall x\in A\left\{y\in B|\phi \right\}\in \mathrm{V}\to \bigcup _{x\in A}\left\{y\in B|\phi \right\}=\bigcup \left\{z|\exists x\in Az=\left\{y\in B|\phi \right\}\right\}$$
10	8 9	syl	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\to \bigcup _{x\in A}\left\{y\in B|\phi \right\}=\bigcup \left\{z|\exists x\in Az=\left\{y\in B|\phi \right\}\right\}$$
11		eqid	$$⊢\left(x\in A⟼\left\{y\in B|\phi \right\}\right)=\left(x\in A⟼\left\{y\in B|\phi \right\}\right)$$
12	11	rnmpt	$$⊢\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)=\left\{z|\exists x\in Az=\left\{y\in B|\phi \right\}\right\}$$
13	12	unieqi	$$⊢\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)=\bigcup \left\{z|\exists x\in Az=\left\{y\in B|\phi \right\}\right\}$$
14	10 13	eqtr4di	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\to \bigcup _{x\in A}\left\{y\in B|\phi \right\}=\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)$$
15		id	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\to \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}$$
16	14 15	eqeltrrd	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\to \bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\in \mathrm{dom}\mathrm{card}$$
17	16	3ad2ant2	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\in \mathrm{dom}\mathrm{card}$$
18		simp3	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \forall x\in A\exists y\in B\phi$$
19		necom	$$⊢\left\{y\in B|\phi \right\}\ne \varnothing \leftrightarrow \varnothing \ne \left\{y\in B|\phi \right\}$$
20		rabn0	$$⊢\left\{y\in B|\phi \right\}\ne \varnothing \leftrightarrow \exists y\in B\phi$$
21		df-ne	$$⊢\varnothing \ne \left\{y\in B|\phi \right\}\leftrightarrow \neg \varnothing =\left\{y\in B|\phi \right\}$$
22	19 20 21	3bitr3i	$$⊢\exists y\in B\phi \leftrightarrow \neg \varnothing =\left\{y\in B|\phi \right\}$$
23	22	ralbii	$$⊢\forall x\in A\exists y\in B\phi \leftrightarrow \forall x\in A\neg \varnothing =\left\{y\in B|\phi \right\}$$
24		ralnex	$$⊢\forall x\in A\neg \varnothing =\left\{y\in B|\phi \right\}\leftrightarrow \neg \exists x\in A\varnothing =\left\{y\in B|\phi \right\}$$
25	23 24	bitri	$$⊢\forall x\in A\exists y\in B\phi \leftrightarrow \neg \exists x\in A\varnothing =\left\{y\in B|\phi \right\}$$
26	18 25	sylib	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \neg \exists x\in A\varnothing =\left\{y\in B|\phi \right\}$$
27		0ex	$$⊢\varnothing \in \mathrm{V}$$
28	11	elrnmpt	$$⊢\varnothing \in \mathrm{V}\to \left(\varnothing \in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\leftrightarrow \exists x\in A\varnothing =\left\{y\in B|\phi \right\}\right)$$
29	27 28	ax-mp	$$⊢\varnothing \in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\leftrightarrow \exists x\in A\varnothing =\left\{y\in B|\phi \right\}$$
30	26 29	sylnibr	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \neg \varnothing \in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)$$
31		ac5num	$$⊢\left(\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\in \mathrm{dom}\mathrm{card}\wedge \neg \varnothing \in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\right)\to \exists g\left(g:\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)⟶\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)$$
32	17 30 31	syl2anc	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \exists g\left(g:\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)⟶\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)$$
33		ffn	$$⊢g:\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)⟶\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\to gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)$$
34	33	anim1i	$$⊢\left(g:\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)⟶\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)\to \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)$$
35	8	3ad2ant2	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \forall x\in A\left\{y\in B|\phi \right\}\in \mathrm{V}$$
36		fveq2	$$⊢z=\left\{y\in B|\phi \right\}\to g\left(z\right)=g\left(\left\{y\in B|\phi \right\}\right)$$
37		id	$$⊢z=\left\{y\in B|\phi \right\}\to z=\left\{y\in B|\phi \right\}$$
38	36 37	eleq12d	$$⊢z=\left\{y\in B|\phi \right\}\to \left(g\left(z\right)\in z\leftrightarrow g\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)$$
39	11 38	ralrnmptw	$$⊢\forall x\in A\left\{y\in B|\phi \right\}\in \mathrm{V}\to \left(\forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\leftrightarrow \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)$$
40	35 39	syl	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \left(\forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\leftrightarrow \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)$$
41	40	anbi2d	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \left(\left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)\leftrightarrow \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)$$
42	34 41	imbitrid	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \left(\left(g:\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)⟶\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)\to \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)$$
43		simpl1	$$⊢\left(\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)\to A\in V$$
44	43	mptexd	$$⊢\left(\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)\to \left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\in \mathrm{V}$$
45		elrabi	$$⊢g\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\to g\left(\left\{y\in B|\phi \right\}\right)\in B$$
46	45	ralimi	$$⊢\forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\to \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in B$$
47	46	ad2antll	$$⊢\left(\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)\to \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in B$$
48		eqid	$$⊢\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)$$
49	48	fmpt	$$⊢\forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in B\leftrightarrow \left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right):A⟶B$$
50	47 49	sylib	$$⊢\left(\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)\to \left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right):A⟶B$$
51		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
52	51	elrabsf	$$⊢g\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\leftrightarrow \left(g\left(\left\{y\in B|\phi \right\}\right)\in B\wedge \underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi \right)$$
53	52	simprbi	$$⊢g\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\to \underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi$$
54	53	ralimi	$$⊢\forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\to \forall x\in A\underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi$$
55	54	ad2antll	$$⊢\left(\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)\to \forall x\in A\underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi$$
56	50 55	jca	$$⊢\left(\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)\to \left(\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right):A⟶B\wedge \forall x\in A\underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi \right)$$
57		feq1	$$⊢f=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\to \left(f:A⟶B\leftrightarrow \left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right):A⟶B\right)$$
58		nfmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)$$
59	58	nfeq2	$$⊢Ⅎxf=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)$$
60		fvex	$$⊢f\left(x\right)\in \mathrm{V}$$
61	60 1	sbcie	$$⊢\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \psi$$
62		fveq1	$$⊢f=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\to f\left(x\right)=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\left(x\right)$$
63		fvex	$$⊢g\left(\left\{y\in B|\phi \right\}\right)\in \mathrm{V}$$
64	48	fvmpt2	$$⊢\left(x\in A\wedge g\left(\left\{y\in B|\phi \right\}\right)\in \mathrm{V}\right)\to \left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\left(x\right)=g\left(\left\{y\in B|\phi \right\}\right)$$
65	63 64	mpan2	$$⊢x\in A\to \left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\left(x\right)=g\left(\left\{y\in B|\phi \right\}\right)$$
66	62 65	sylan9eq	$$⊢\left(f=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\wedge x\in A\right)\to f\left(x\right)=g\left(\left\{y\in B|\phi \right\}\right)$$
67	66	sbceq1d	$$⊢\left(f=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\wedge x\in A\right)\to \left(\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi \right)$$
68	61 67	bitr3id	$$⊢\left(f=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\wedge x\in A\right)\to \left(\psi \leftrightarrow \underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi \right)$$
69	59 68	ralbida	$$⊢f=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\to \left(\forall x\in A\psi \leftrightarrow \forall x\in A\underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi \right)$$
70	57 69	anbi12d	$$⊢f=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\to \left(\left(f:A⟶B\wedge \forall x\in A\psi \right)\leftrightarrow \left(\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right):A⟶B\wedge \forall x\in A\underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi \right)\right)$$
71	44 56 70	spcedv	$$⊢\left(\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$
72	71	ex	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \left(\left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)\right)$$
73	42 72	syld	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \left(\left(g:\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)⟶\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)\right)$$
74	73	exlimdv	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \left(\exists g\left(g:\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)⟶\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)\right)$$
75	32 74	mpd	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$